安全案例提供清晰、全面和可靠的论据,说明系统在特定环境下的操作满足可接受的安全性.在受监管的安全攸关领域,如汽车、航空和核能等领域,认证机构通常要求系统经过严格的安全评估程序,以确保其符合一个或多个安全标准.在系统开发中应...安全案例提供清晰、全面和可靠的论据,说明系统在特定环境下的操作满足可接受的安全性.在受监管的安全攸关领域,如汽车、航空和核能等领域,认证机构通常要求系统经过严格的安全评估程序,以确保其符合一个或多个安全标准.在系统开发中应用安全案例是一种新兴的技术手段,以结构化和全面的方式表达安全攸关系统的安全属性.对安全案例的4个基本构建步骤:确定目标、收集证据、构建论证和评估安全案例,进行简要介绍.然后聚焦于构建论证这一关键步骤,详细介绍现有的8种安全案例表达形式,包括目标结构符号(GSN)、声明-论点-证据(CAE)、结构化安全案例元模型(SACM)等,并分析了它们的优缺点.由于安全案例所需材料的显著复杂性,软件工具通常被用作构建和评估安全案例的实用方法.比较7种用于安全案例开发和评估的工具,包括astah system safety、gsn2x、NOR-STA、Socrates、ASCE、D-Case Editor和AdvoCATE.此外,还深入探讨了安全案例构建中所面临的多重挑战,这些挑战包括数据的可靠性和完整性、复杂性和不确定性的管理、监管和标准的不一致、人因工程、技术的快速发展以及团队和跨学科合作6个方面.最后,展望安全案例的未来研究方向,揭示其潜在应用和研究问题.展开更多
An algorithm for the verification of strong open bisimulation in π-calculus with mismatch was presented, which is based on the symbolic transition graph (STG). Given two processes, we can convert them into two STGs b...An algorithm for the verification of strong open bisimulation in π-calculus with mismatch was presented, which is based on the symbolic transition graph (STG). Given two processes, we can convert them into two STGs by a set of rules at first. Next, the algorithm computes a predicate equation system (PES) from the STGs. This is the key step of the whole algorithm. Finally, the PES is solved and the greatest symbolic solution is got. Correctness of the algorithm is proved and time complexity discussed. It is shown that the worst-case time complexity is exponential.展开更多
In order to analyze the trustworthiness of complex software systems,we propose a model of evidence-based software trustworthiness called trustworthiness derivation tree(TDT).The basic idea of constructing a TDT is to ...In order to analyze the trustworthiness of complex software systems,we propose a model of evidence-based software trustworthiness called trustworthiness derivation tree(TDT).The basic idea of constructing a TDT is to refine main properties into key ingredients and continue the refinement until basic facts such as evidences are reached.The skeleton of a TDT can be specified by a set of rules,which are convenient for automated reasoning in Prolog.We develop a visualization tool that can construct the skeleton of a TDT by taking the rules as input,and allow a user to edit the TDT in a graphical user interface.In a software development life cycle,TDTs can serve as a communication means for different stakeholders to agree on the properties about a system in the requirement analysis phase,and they can be used for deductive reasoning so as to verify whether the system achieves trustworthiness in the product validation phase.We have piloted the approach of using TDTs in more than a dozen real scenarios of software development.Indeed,using TDTs helped us to discover and then resolve some subtle problems.展开更多
The goal of qubit mapping is to map a logical circuit to a physical device by introducing additional gates as few as possible in an acceptable amount of time.We present an effective approach called Tabu Search Based A...The goal of qubit mapping is to map a logical circuit to a physical device by introducing additional gates as few as possible in an acceptable amount of time.We present an effective approach called Tabu Search Based Adjustment(TSA)algorithm to construct the mappings.It consists of two key steps:one is making use of a combined subgraph isomorphism and completion to initialize some candidate mappings,and the other is dynamically modifying the mappings by TSA.Our experiments show that,compared with state-of-the-art methods,TSA can generate mappings with a smaller number of additional gates and have better scalability for large-scale circuits.展开更多
We extend the traditional nonnegative reward testing with negative rewards.In this new testing framework,may preorder and must preorder are the inverse of each other.More surprisingly,it turns out that the real reward...We extend the traditional nonnegative reward testing with negative rewards.In this new testing framework,may preorder and must preorder are the inverse of each other.More surprisingly,it turns out that the real reward must testing is no more powerful than the nonnegative reward testing,at least for finite processes. In order to prove that result,we exploit an important property of failure simulation about the inclusion of the testing outcomes between two related processes.展开更多
This paper focuses on the problem of seeking complete axiomatization for finite processes in the process calculus called symbolic probabilistic π-calculus introduced by Wu,Palamidessi and Lin.We provide inference sys...This paper focuses on the problem of seeking complete axiomatization for finite processes in the process calculus called symbolic probabilistic π-calculus introduced by Wu,Palamidessi and Lin.We provide inference systems for both strong and weak symbolic probabilistic bisimulations and also prove their soundness and completeness.This is the first work,to our knowledge,that provides complete axiomatization for symbolic probabilistic bisimulations in the presence of both nondeterministic and probabilistic choice.展开更多
文摘安全案例提供清晰、全面和可靠的论据,说明系统在特定环境下的操作满足可接受的安全性.在受监管的安全攸关领域,如汽车、航空和核能等领域,认证机构通常要求系统经过严格的安全评估程序,以确保其符合一个或多个安全标准.在系统开发中应用安全案例是一种新兴的技术手段,以结构化和全面的方式表达安全攸关系统的安全属性.对安全案例的4个基本构建步骤:确定目标、收集证据、构建论证和评估安全案例,进行简要介绍.然后聚焦于构建论证这一关键步骤,详细介绍现有的8种安全案例表达形式,包括目标结构符号(GSN)、声明-论点-证据(CAE)、结构化安全案例元模型(SACM)等,并分析了它们的优缺点.由于安全案例所需材料的显著复杂性,软件工具通常被用作构建和评估安全案例的实用方法.比较7种用于安全案例开发和评估的工具,包括astah system safety、gsn2x、NOR-STA、Socrates、ASCE、D-Case Editor和AdvoCATE.此外,还深入探讨了安全案例构建中所面临的多重挑战,这些挑战包括数据的可靠性和完整性、复杂性和不确定性的管理、监管和标准的不一致、人因工程、技术的快速发展以及团队和跨学科合作6个方面.最后,展望安全案例的未来研究方向,揭示其潜在应用和研究问题.
基金National Natural Science Foundation of China ( No. 6 98730 32 ) 86 3Hi-Τ ech Project ( 86 3-30 6 -ZT-0 6 -0 2 -2 )
文摘An algorithm for the verification of strong open bisimulation in π-calculus with mismatch was presented, which is based on the symbolic transition graph (STG). Given two processes, we can convert them into two STGs by a set of rules at first. Next, the algorithm computes a predicate equation system (PES) from the STGs. This is the key step of the whole algorithm. Finally, the PES is solved and the greatest symbolic solution is got. Correctness of the algorithm is proved and time complexity discussed. It is shown that the worst-case time complexity is exponential.
基金the National Natural Science Foundation of China (Nos.61832015 and 62072176)the Inria-CAS Joint Project Quasar and Shanghai Trusted Industry Internet Software Collaborative Innovation Center。
文摘In order to analyze the trustworthiness of complex software systems,we propose a model of evidence-based software trustworthiness called trustworthiness derivation tree(TDT).The basic idea of constructing a TDT is to refine main properties into key ingredients and continue the refinement until basic facts such as evidences are reached.The skeleton of a TDT can be specified by a set of rules,which are convenient for automated reasoning in Prolog.We develop a visualization tool that can construct the skeleton of a TDT by taking the rules as input,and allow a user to edit the TDT in a graphical user interface.In a software development life cycle,TDTs can serve as a communication means for different stakeholders to agree on the properties about a system in the requirement analysis phase,and they can be used for deductive reasoning so as to verify whether the system achieves trustworthiness in the product validation phase.We have piloted the approach of using TDTs in more than a dozen real scenarios of software development.Indeed,using TDTs helped us to discover and then resolve some subtle problems.
基金supported by the National Natural Science Foundation of China under Grant Nos.61832015,62072176,12271172 and 11871221the Research Funds of Happiness Flower of East China Normal University under Grant No.2020ECNU-XFZH005+1 种基金the Fundamental Research Funds for the Central Universities of China under Grant No.2021JQRH014Shanghai Trusted Industry Internet Software Collaborative Innovation Center,and the “Digital Silk Road”Shanghai International Joint Lab of Trustworthy Intelligent Software under Grant No.22510750100.
文摘The goal of qubit mapping is to map a logical circuit to a physical device by introducing additional gates as few as possible in an acceptable amount of time.We present an effective approach called Tabu Search Based Adjustment(TSA)algorithm to construct the mappings.It consists of two key steps:one is making use of a combined subgraph isomorphism and completion to initialize some candidate mappings,and the other is dynamically modifying the mappings by TSA.Our experiments show that,compared with state-of-the-art methods,TSA can generate mappings with a smaller number of additional gates and have better scalability for large-scale circuits.
基金the National Natural Science Foundation of China(No.61033002)
文摘We extend the traditional nonnegative reward testing with negative rewards.In this new testing framework,may preorder and must preorder are the inverse of each other.More surprisingly,it turns out that the real reward must testing is no more powerful than the nonnegative reward testing,at least for finite processes. In order to prove that result,we exploit an important property of failure simulation about the inclusion of the testing outcomes between two related processes.
基金the National Basic Research Program (973) of China (No.2003CB317005)the National Nature Science Foundation of China (Nos.60573002 and 60703033)
文摘This paper focuses on the problem of seeking complete axiomatization for finite processes in the process calculus called symbolic probabilistic π-calculus introduced by Wu,Palamidessi and Lin.We provide inference systems for both strong and weak symbolic probabilistic bisimulations and also prove their soundness and completeness.This is the first work,to our knowledge,that provides complete axiomatization for symbolic probabilistic bisimulations in the presence of both nondeterministic and probabilistic choice.
