Timed abstract state machine(TASM) is a formal specification language used to specify and simulate the behavior of real-time systems. Formal verification of TASM model can be fulfilled through model checking activitie...Timed abstract state machine(TASM) is a formal specification language used to specify and simulate the behavior of real-time systems. Formal verification of TASM model can be fulfilled through model checking activities by translating into UPPAAL. Firstly, the translational semantics from TASM to UPPAAL is presented through atlas transformation language(ATL). Secondly, the implementation of the proposed model transformation tool TASM2UPPAAL is provided. Finally, a case study is given to illustrate the automatic transformation from TASM model to UPPAAL model.展开更多
Ensuring the correctness and reliability of large-scale resource sharing and complex job processing Is an Important task for grid applications. From a formal method perspective, a grid service chain model based on sta...Ensuring the correctness and reliability of large-scale resource sharing and complex job processing Is an Important task for grid applications. From a formal method perspective, a grid service chain model based on state PI calculus Is proposed In this work as the theoretical foundation for the service composition and collaboration in grid. Following the Idea of the Web Service Resource Framework （WSRF）, state PI calculus enables the life-cycle management of system states by associating the actions in the original PI calculus with system states. Moreover, model checking technique is exploltad for the design-time and run-time logical verification of grid service chain models. A grid application scenario of the dynamic analysis of material deformation structure is also provided to show the effectiveness of the proposed work.展开更多
High reliability is the key to performance of electrical control equipment. PLC combines computer technology, automatic control technology and communication technology and becomes widely used for automation of industr...High reliability is the key to performance of electrical control equipment. PLC combines computer technology, automatic control technology and communication technology and becomes widely used for automation of industrial processes. Some requirements of complex PLC systems cannot be satisfied by the traditional verification methods. In this paper, an efficient method for the PLC systems modeling and verification is proposed. To ensure the high-speed property of PLC, we proposed a technique of “Time interval model” and “notice-waiting”. It could reduce the state space and make it possible to verify some complex PLC systems. Also, the conversion from the built PLC model to the Promela language is obtained and a tool PLC-Checker for modeling and checking PLC systems are designed. Using PLC-Checker to check a classical PLC example, a counter-example is found. Although the probability of this logic error occurs very small, it could result in system crash fatally.展开更多
SAT-based bounded model checking （BMC） has been introduced as a complementary technique to BDD-based symbolic model checking in recent years, and a lot of successful work has been done in this direction. The approac...SAT-based bounded model checking （BMC） has been introduced as a complementary technique to BDD-based symbolic model checking in recent years, and a lot of successful work has been done in this direction. The approach was first introduced by A. Biere et al. in checking linear temporal logic （LTL） formulae and then also adapted to check formulae of the universal fragment of computation tree logic （ACTL） by W. Penczek et al. As the efficiency of model checking is still an important issue, we present an improved BMC approach for ACTL based on Penczek＇s method. We consider two aspects of the approach. One is reduction of the number of variables and transitions in the κ-model by distinguishing the temporal operator EX from the others. The other is simplification of the transformation of formulae by using uniform path encoding instead of a disjunction of all paths needed in the κ-model. With these improvements, for an ACTL formula, the length of the final encoding of the formula in the worst case is reduced. The improved approach is implemented in the tool BMV and is compared with the original one by applying both to two well known examples, mutual exclusion and dining philosophers. The comparison shoves the advantages of the improved approach with respect to the efficiency of model checking.展开更多
Most of the timed automata reachability analysis algorithms in the literature explore the state spaces by enumeration of symbolic states, which use time constraints to represent a set of concrete states. A time constr...Most of the timed automata reachability analysis algorithms in the literature explore the state spaces by enumeration of symbolic states, which use time constraints to represent a set of concrete states. A time constraint is a conjunction of atomic formulas which bound the differences of clock values. In this paper, it is shown that some atomic formulas of symbolic states generated by the algorithms can be removed to improve the model checking time- and spaceefficiency. Such atomic formulas are called as irrelevant atomic formulas. A method is also presented to detect irrelevant formulas based on the test-reset information about clock variables. An optimized model-checking algorithm is designed based on these techniques. The case studies show that the techniques presented in this paper significantly improve the space- and time-efficlency of reachability analysis.展开更多
In this paper, a scheme of combining model checking and theorem proving techniques to verify high trustworthy embedded software is proposed. The software model described in state machine of unified model language is t...In this paper, a scheme of combining model checking and theorem proving techniques to verify high trustworthy embedded software is proposed. The software model described in state machine of unified model language is transformed into the input modeling language of a model checker in which the model is analyzed with associated property specifications expressed in temporal logic. The software model which has been verified by model checker is then transformed into abstract specifications of a theorem prover , in which the model will be refined, verified and translated into source C code. The transformation rules from state machine to input language of model checker and abstract specifications of theorem prover are given. The experiment shows that the proposed scheme can effectively improve the development and verification of high trustworthy embedded software.展开更多
The formal modeling and verification of aircraft takeoff is a challenge because it is a complex safety-critical operation.The task of aircraft takeoff is distributed amongst various computer-based controllers,however,...The formal modeling and verification of aircraft takeoff is a challenge because it is a complex safety-critical operation.The task of aircraft takeoff is distributed amongst various computer-based controllers,however,with the growing malicious threats a secure communication between aircraft and controllers becomes highly important.This research serves as a starting point for integration of BB84 quantum protocol with petri nets for secure modeling and verification of takeoff procedure.The integrated model combines the BB84 quantum cryptographic protocol with powerful verification tool support offered by petri nets.To model certain important properties of BB84,a new variant of petri nets coined as Quantum Nets are proposed by defining their mathematical foundations and overall system dynamics,furthermore,some important system properties are also abstractly defined.The proposed QuantumNets are then applied for modeling of aircraft takeoff process by defining three quantum nets:namely aircraft,runway controller and gate controller.For authentication between quantum nets,the use of external places and transitions is demonstrated to describe the encryptiondecryption process of qubits stream.Finally,the developed takeoff quantum network is verified through simulation offered by colored petri-net(CPN)Tools.Moreover,reachability tree(RT)analysis is also performed to have greater confidence in feasibility and correctness of the proposed aircraft takeoff model through the Quantum Nets.展开更多
A multi-agent based transport system is modeled by timed automata model extended with clock variables. The correctness properties of safety and liveness of this model are verified by timed automata based UPPAAL. Agent...A multi-agent based transport system is modeled by timed automata model extended with clock variables. The correctness properties of safety and liveness of this model are verified by timed automata based UPPAAL. Agents have a degree of control on their own actions, have their own threads of control, and under some circumstances they are also able to take decisions. Therefore they are autonomous. The multi-agent system is modeled as a network of timed automata based agents supported by clock variables. The representation of agent requirements based on mathematics is helpful in precise and unambiguous specifications, thereby ensuring correctness. This formal representation of requirements provides a way for logical reasoning about the artifacts produced. We can be systematic and precise in assessing correctness by rigorously specifying the functional requirements.展开更多
Graph transformation systems have become a general formal modeling language to describe many models in software development process.Behavioral modeling of dynamic systems and model-to-model transformations are only a ...Graph transformation systems have become a general formal modeling language to describe many models in software development process.Behavioral modeling of dynamic systems and model-to-model transformations are only a few examples in which graphs have been used to software development.But even the perfect graph transformation system must be equipped with automated analysis capabilities to let users understand whether such a formal specification fulfills their requirements.In this paper,we present a new solution to verify graph transformation systems using the Bogor model checker.The attributed graph grammars(AGG)-like graph transformation systems are translated to Bandera intermediate representation(BIR),the input language of Bogor,and Bogor verifies the model against some interesting properties defined by combining linear temporal logic(LTL) and special-purpose graph rules.Experimental results are encouraging,showing that in most cases our solution improves existing approaches in terms of both performance and expressiveness.展开更多
Web Services Choreography Description Language lacks a formal system to accurately express the semantics of service behaviors and verify the correctness of a service choreography model.This paper presents a new approa...Web Services Choreography Description Language lacks a formal system to accurately express the semantics of service behaviors and verify the correctness of a service choreography model.This paper presents a new approach of choreography model verification based on Description Logic.A meta model of service choreography is built to provide a conceptual framework to capture the formal syntax and semantics of service choreography.Based on the framework,a set of rules and constraints are defined in Description Logic for choreography model verification.To automate model verification,the UML-based service choreography model will be transformed,by the given algorithms,into the DL-based ontology,and thus the model properties can be verified by reasoning through the ontology with the help of a popular DL reasoned.A case study is given to demonstrate applicability of the method.Furthermore,the work will be compared with other related research.展开更多
In traditional digital twin communication system testing,we can apply test cases as completely as possible in order to ensure the correctness of the system implementation,and even then,there is no guarantee that the d...In traditional digital twin communication system testing,we can apply test cases as completely as possible in order to ensure the correctness of the system implementation,and even then,there is no guarantee that the digital twin communication system implementation is completely correct.Formal verification is currently recognized as a method to ensure the correctness of software system for communication in digital twins because it uses rigorous mathematical methods to verify the correctness of systems for communication in digital twins and can effectively help system designers determine whether the system is designed and implemented correctly.In this paper,we use the interactive theorem proving tool Isabelle/HOL to construct the formal model of the X86 architecture,and to model the related assembly instructions.The verification result shows that the system states obtained after the operations of relevant assembly instructions is consistent with the expected states,indicating that the system meets the design expectations.展开更多
Projection temporal logic(PTL) is an extension of interval temporal logic(ITL) with a new projection operator prj and infinite intervals which has been well investigated in the past ten years.In this paper,we review t...Projection temporal logic(PTL) is an extension of interval temporal logic(ITL) with a new projection operator prj and infinite intervals which has been well investigated in the past ten years.In this paper,we review the work on PTL in four aspects:(1) decidability,complexity and expressiveness of propositional PTL(PPTL);(2) modeling,simulation and verification language(MSVL);(3) formal verification approaches with MSVL and PPTL;and(4) supporting toolkit MSV.展开更多
As a complementary technology to Binary Decision Diagram-based(BDD-based) symbolic model checking, the verification techniques on Boolean satisfiability problem have gained an increasing wide of applications over the ...As a complementary technology to Binary Decision Diagram-based(BDD-based) symbolic model checking, the verification techniques on Boolean satisfiability problem have gained an increasing wide of applications over the last few decades, which brings a dramatic improvement for automatic verification. In this paper, we firstly introduce the theory about the Boolean satisfiability verification, including the description on the problem of Boolean satisfiability verification, Davis-Putnam-Logemann-Loveland(DPLL) based complete verification algorithm, and all kinds of solvers generated and the logic languages used by those solvers. Moreover, we formulate a large number optimizations of technique revolutions based on Boolean SATisfiability(SAT) and Satisfiability Modulo Theories(SMT) solving in detail, including incomplete methods such as bounded model checking, and other methods for concurrent programs model checking. Finally, we point out the major challenge pervasively in industrial practice and prospect directions for future research in the field of formal verification.展开更多
This paper presents the formal specification and model-checklng of Carrier Sense Multiple Access with Collision Avoidance（ CSMA/CA） protocol using the model checker we developed for real-time systems, which are spec...This paper presents the formal specification and model-checklng of Carrier Sense Multiple Access with Collision Avoidance（ CSMA/CA） protocol using the model checker we developed for real-time systems, which are specified as networks of finite precision timed automata. The CSMA/CA protocol proposed in the IEEE 802.11 standard is designed to reduce the probability of collision during a transmission in wireless random access environments. However, it does not eliminate completely the possibility of a collision between two or more frames transmitted simultaneously. We investigate what will give rise to a collision between frames and use our automatic verification tool for model-checking.展开更多
基金National Natural Science Foundations of China(No. 61073013,No. 90818024)Aviation Science Foundation of China( No.2010ZAO4001)
文摘Timed abstract state machine(TASM) is a formal specification language used to specify and simulate the behavior of real-time systems. Formal verification of TASM model can be fulfilled through model checking activities by translating into UPPAAL. Firstly, the translational semantics from TASM to UPPAAL is presented through atlas transformation language(ATL). Secondly, the implementation of the proposed model transformation tool TASM2UPPAAL is provided. Finally, a case study is given to illustrate the automatic transformation from TASM model to UPPAAL model.
基金Supported by the National Natural Science Foundation of China (Grant Nos. 60604033 and 60553001)
文摘Ensuring the correctness and reliability of large-scale resource sharing and complex job processing Is an Important task for grid applications. From a formal method perspective, a grid service chain model based on state PI calculus Is proposed In this work as the theoretical foundation for the service composition and collaboration in grid. Following the Idea of the Web Service Resource Framework （WSRF）, state PI calculus enables the life-cycle management of system states by associating the actions in the original PI calculus with system states. Moreover, model checking technique is exploltad for the design-time and run-time logical verification of grid service chain models. A grid application scenario of the dynamic analysis of material deformation structure is also provided to show the effectiveness of the proposed work.
文摘High reliability is the key to performance of electrical control equipment. PLC combines computer technology, automatic control technology and communication technology and becomes widely used for automation of industrial processes. Some requirements of complex PLC systems cannot be satisfied by the traditional verification methods. In this paper, an efficient method for the PLC systems modeling and verification is proposed. To ensure the high-speed property of PLC, we proposed a technique of “Time interval model” and “notice-waiting”. It could reduce the state space and make it possible to verify some complex PLC systems. Also, the conversion from the built PLC model to the Promela language is obtained and a tool PLC-Checker for modeling and checking PLC systems are designed. Using PLC-Checker to check a classical PLC example, a counter-example is found. Although the probability of this logic error occurs very small, it could result in system crash fatally.
基金supported by the National Natural Science Foundation of China under Grants No.60573012 and No.60721061the National Basic Research 973 Program of China under Grant No.2002CB312200.
文摘SAT-based bounded model checking （BMC） has been introduced as a complementary technique to BDD-based symbolic model checking in recent years, and a lot of successful work has been done in this direction. The approach was first introduced by A. Biere et al. in checking linear temporal logic （LTL） formulae and then also adapted to check formulae of the universal fragment of computation tree logic （ACTL） by W. Penczek et al. As the efficiency of model checking is still an important issue, we present an improved BMC approach for ACTL based on Penczek＇s method. We consider two aspects of the approach. One is reduction of the number of variables and transitions in the κ-model by distinguishing the temporal operator EX from the others. The other is simplification of the transformation of formulae by using uniform path encoding instead of a disjunction of all paths needed in the κ-model. With these improvements, for an ACTL formula, the length of the final encoding of the formula in the worst case is reduced. The improved approach is implemented in the tool BMV and is compared with the original one by applying both to two well known examples, mutual exclusion and dining philosophers. The comparison shoves the advantages of the improved approach with respect to the efficiency of model checking.
基金Supported by the National Natural Science Foundation of China （Grant Nos. 60203009, 60233020 and 60425204）, the NSF of Jiangsu Province （Grant No. BK2003408） and the National Basic Research 973 Program of China （Grant No. 2002CB312001）.
文摘Most of the timed automata reachability analysis algorithms in the literature explore the state spaces by enumeration of symbolic states, which use time constraints to represent a set of concrete states. A time constraint is a conjunction of atomic formulas which bound the differences of clock values. In this paper, it is shown that some atomic formulas of symbolic states generated by the algorithms can be removed to improve the model checking time- and spaceefficiency. Such atomic formulas are called as irrelevant atomic formulas. A method is also presented to detect irrelevant formulas based on the test-reset information about clock variables. An optimized model-checking algorithm is designed based on these techniques. The case studies show that the techniques presented in this paper significantly improve the space- and time-efficlency of reachability analysis.
基金This workis Supported by the National High-Technology Research and Development Program(863-301-05-03) .
文摘In this paper, a scheme of combining model checking and theorem proving techniques to verify high trustworthy embedded software is proposed. The software model described in state machine of unified model language is transformed into the input modeling language of a model checker in which the model is analyzed with associated property specifications expressed in temporal logic. The software model which has been verified by model checker is then transformed into abstract specifications of a theorem prover , in which the model will be refined, verified and translated into source C code. The transformation rules from state machine to input language of model checker and abstract specifications of theorem prover are given. The experiment shows that the proposed scheme can effectively improve the development and verification of high trustworthy embedded software.
文摘The formal modeling and verification of aircraft takeoff is a challenge because it is a complex safety-critical operation.The task of aircraft takeoff is distributed amongst various computer-based controllers,however,with the growing malicious threats a secure communication between aircraft and controllers becomes highly important.This research serves as a starting point for integration of BB84 quantum protocol with petri nets for secure modeling and verification of takeoff procedure.The integrated model combines the BB84 quantum cryptographic protocol with powerful verification tool support offered by petri nets.To model certain important properties of BB84,a new variant of petri nets coined as Quantum Nets are proposed by defining their mathematical foundations and overall system dynamics,furthermore,some important system properties are also abstractly defined.The proposed QuantumNets are then applied for modeling of aircraft takeoff process by defining three quantum nets:namely aircraft,runway controller and gate controller.For authentication between quantum nets,the use of external places and transitions is demonstrated to describe the encryptiondecryption process of qubits stream.Finally,the developed takeoff quantum network is verified through simulation offered by colored petri-net(CPN)Tools.Moreover,reachability tree(RT)analysis is also performed to have greater confidence in feasibility and correctness of the proposed aircraft takeoff model through the Quantum Nets.
文摘A multi-agent based transport system is modeled by timed automata model extended with clock variables. The correctness properties of safety and liveness of this model are verified by timed automata based UPPAAL. Agents have a degree of control on their own actions, have their own threads of control, and under some circumstances they are also able to take decisions. Therefore they are autonomous. The multi-agent system is modeled as a network of timed automata based agents supported by clock variables. The representation of agent requirements based on mathematics is helpful in precise and unambiguous specifications, thereby ensuring correctness. This formal representation of requirements provides a way for logical reasoning about the artifacts produced. We can be systematic and precise in assessing correctness by rigorously specifying the functional requirements.
文摘Graph transformation systems have become a general formal modeling language to describe many models in software development process.Behavioral modeling of dynamic systems and model-to-model transformations are only a few examples in which graphs have been used to software development.But even the perfect graph transformation system must be equipped with automated analysis capabilities to let users understand whether such a formal specification fulfills their requirements.In this paper,we present a new solution to verify graph transformation systems using the Bogor model checker.The attributed graph grammars(AGG)-like graph transformation systems are translated to Bandera intermediate representation(BIR),the input language of Bogor,and Bogor verifies the model against some interesting properties defined by combining linear temporal logic(LTL) and special-purpose graph rules.Experimental results are encouraging,showing that in most cases our solution improves existing approaches in terms of both performance and expressiveness.
基金This work is supported by the National Natural Science Fund number 61802428.
文摘Web Services Choreography Description Language lacks a formal system to accurately express the semantics of service behaviors and verify the correctness of a service choreography model.This paper presents a new approach of choreography model verification based on Description Logic.A meta model of service choreography is built to provide a conceptual framework to capture the formal syntax and semantics of service choreography.Based on the framework,a set of rules and constraints are defined in Description Logic for choreography model verification.To automate model verification,the UML-based service choreography model will be transformed,by the given algorithms,into the DL-based ontology,and thus the model properties can be verified by reasoning through the ontology with the help of a popular DL reasoned.A case study is given to demonstrate applicability of the method.Furthermore,the work will be compared with other related research.
基金supported in part by the Natural Science Foundation of Jiangsu Province in China under grant No.BK20191475the fifth phase of“333 Project”scientific research funding project of Jiangsu Province in China under grant No.BRA2020306the Qing Lan Project of Jiangsu Province in China under grant No.2019.
文摘In traditional digital twin communication system testing,we can apply test cases as completely as possible in order to ensure the correctness of the system implementation,and even then,there is no guarantee that the digital twin communication system implementation is completely correct.Formal verification is currently recognized as a method to ensure the correctness of software system for communication in digital twins because it uses rigorous mathematical methods to verify the correctness of systems for communication in digital twins and can effectively help system designers determine whether the system is designed and implemented correctly.In this paper,we use the interactive theorem proving tool Isabelle/HOL to construct the formal model of the X86 architecture,and to model the related assembly instructions.The verification result shows that the system states obtained after the operations of relevant assembly instructions is consistent with the expected states,indicating that the system meets the design expectations.
基金supported by the National Natural Science Foundation of China(Grant Nos.61133001,61272117,61202038,61322202,61420106004 and 91418201)
文摘Projection temporal logic(PTL) is an extension of interval temporal logic(ITL) with a new projection operator prj and infinite intervals which has been well investigated in the past ten years.In this paper,we review the work on PTL in four aspects:(1) decidability,complexity and expressiveness of propositional PTL(PPTL);(2) modeling,simulation and verification language(MSVL);(3) formal verification approaches with MSVL and PPTL;and(4) supporting toolkit MSV.
基金Supported by the National Natural Science Foundation of China(Nos.61063002,61100186,61262008)Guangxi Natural Science Foundation of China(2011GXNSFA018164,2011GXNSFA018166,2012GXNSFAA053220)the Key Project of Education Department of Guangxi
文摘As a complementary technology to Binary Decision Diagram-based(BDD-based) symbolic model checking, the verification techniques on Boolean satisfiability problem have gained an increasing wide of applications over the last few decades, which brings a dramatic improvement for automatic verification. In this paper, we firstly introduce the theory about the Boolean satisfiability verification, including the description on the problem of Boolean satisfiability verification, Davis-Putnam-Logemann-Loveland(DPLL) based complete verification algorithm, and all kinds of solvers generated and the logic languages used by those solvers. Moreover, we formulate a large number optimizations of technique revolutions based on Boolean SATisfiability(SAT) and Satisfiability Modulo Theories(SMT) solving in detail, including incomplete methods such as bounded model checking, and other methods for concurrent programs model checking. Finally, we point out the major challenge pervasively in industrial practice and prospect directions for future research in the field of formal verification.
基金The workreportedinthis paperissupported bythe National Grand Fundamental Research973 Programof China (2002cb312200) ,andthe National Nat-ural Science Foundation of China(60242002 ,60273025)
文摘This paper presents the formal specification and model-checklng of Carrier Sense Multiple Access with Collision Avoidance（ CSMA/CA） protocol using the model checker we developed for real-time systems, which are specified as networks of finite precision timed automata. The CSMA/CA protocol proposed in the IEEE 802.11 standard is designed to reduce the probability of collision during a transmission in wireless random access environments. However, it does not eliminate completely the possibility of a collision between two or more frames transmitted simultaneously. We investigate what will give rise to a collision between frames and use our automatic verification tool for model-checking.
