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.展开更多
Various extensions of UML have been developed to meet the challenges of designing modern software systems, such as agent based electronic commerce applications. Recent advances in model checking technology have led i...Various extensions of UML have been developed to meet the challenges of designing modern software systems, such as agent based electronic commerce applications. Recent advances in model checking technology have led it to be introduced into the development of approaches and tools to check the correctness of electronic commerce protocols. This paper focuses on the research of a method that connects an extension of AUML to model checker SPIN/Promela for the specification and verification of agent interaction protocols (AIP) in electronic commerce. The method presented here allows us to combine the benefits of visual specification with the power of some static analysis and model checking. Some algorithms and rules are developed to permit all visual modeling constructs translated mechanically into some Promela models of AIP, as supported by the model checker SPIN. Moreover, a process is illustrated to guide the specification and verification of AIP. The method is demonstrated thoroughly using the e commerce protocol NetBill as an example.展开更多
Recent development on distributed systems has shown that a variety of fairness constraints （some of which are only recently defined） play vital roles in designing self- stabilizing population protocols. Existing mod...Recent development on distributed systems has shown that a variety of fairness constraints （some of which are only recently defined） play vital roles in designing self- stabilizing population protocols. Existing model checkers are deficient in verifying the systems as only limited kinds of fair- ness are supported with limited verification efficiency. In this work, we support model checking of distributed systems in the toolkit PAT （process analysis toolkit）, with a variety of fairness constraints （e.g., process-level weak/strong fairness, event-level weak/strong fairness, strong global fairness）. It performs on-the-fly verification against linear temporal prop- erties. We show through empirical evaluation （on recent pop- ulation protocols as well as benchmark systems） that PAT has advantage in model checking with fairness. Previously un- known bugs have been revealed against systems which are designed to function only with strong global fairness.展开更多
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.展开更多
Based on the authentication tests and the strand space model, the robust email protocol with perfect forward secrecy is formally analyzed, and the security shortcomings of the protocol is pointed out. Meanwhile, the m...Based on the authentication tests and the strand space model, the robust email protocol with perfect forward secrecy is formally analyzed, and the security shortcomings of the protocol is pointed out. Meanwhile, the man-in-the-middle attack to the protocol is given, where the attacker forges the messages in the receiving phase to cheat the two communication parties and makes them share the wrong session keys with him. Therefore, the protocol is not ensured to provide perfect forward secrecy. In order to overcome the above security shortcomings, an advanced email protocol is proposed, where the corresponding signatures in the receiving phase of the protocol are added to overcome the man-in-the-middle attack and ensure to provide perfect forward secrecy. Finally, the proposed advanced email protocol is formally analyzed with the authentication tests and the strand space model, and it is proved to be secure in authentication of the email sender, the recipient and the server. Therefore, the proposed advanced email protocol can really provide perfect forward secrecy.展开更多
Exceptions are those abnormal data flow which needs additional calculation to deal with. Exception analysis concerned abnormal flow contains a lot of research content, such as exception analysis method, program verifi...Exceptions are those abnormal data flow which needs additional calculation to deal with. Exception analysis concerned abnormal flow contains a lot of research content, such as exception analysis method, program verification. This article introduces another research direction of exception analysis which based on formal method. The article analyses and summarizes those research literatures referring exception analysis and exception handling logic verification based on formal reasoning and model checking. In the article, we provide an overview of the relationship and difference between traditional ideas and formal method concerning program exception analysis. In the end of the article, we make some ideas about exception analysis based on formal semantic study of procedure calls. Exception handling is seen as a special semantic effect of procedures calls.展开更多
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.展开更多
Having a formal model of neural networks can greatly help in understanding and verifying their properties,behavior,and response to external factors such as disease and medicine.In this paper,we adopt a formal model to...Having a formal model of neural networks can greatly help in understanding and verifying their properties,behavior,and response to external factors such as disease and medicine.In this paper,we adopt a formal model to represent neurons,some neuronal graphs,and their composition.Some specific neuronal graphs are known for having biologically relevant structures and behaviors and we call them archetypes.These archetypes are supposed to be the basis of typical instances of neuronal information processing.In this paper we study six fundamental archetypes(simple series,series with multiple outputs,parallel composition,negative loop,inhibition of a behavior,and contralateral inhibition),and we consider two ways to couple two archetypes:(i)connecting the output(s)of the first archetype to the input(s)of the second archetype and(ii)nesting the first archetype within the second one.We report and compare two key approaches to the formal modeling and verification of the proposed neuronal archetypes and some selected couplings.The first approach exploits the synchronous programming language Lustre to encode archetypes and their couplings,and to express properties concerning their dynamic behavior.These properties are verified thanks to the use of model checkers.The second approach relies on a theorem prover,the Coq Proof Assistant,to prove dynamic properties of neurons and archetypes.展开更多
文摘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 Research Grants Council of Hong Kong(DAG99/0 0 .EG0 5 ) the Sino-French Advanced ResearchProgram 2 0 0 0 (PR
文摘Various extensions of UML have been developed to meet the challenges of designing modern software systems, such as agent based electronic commerce applications. Recent advances in model checking technology have led it to be introduced into the development of approaches and tools to check the correctness of electronic commerce protocols. This paper focuses on the research of a method that connects an extension of AUML to model checker SPIN/Promela for the specification and verification of agent interaction protocols (AIP) in electronic commerce. The method presented here allows us to combine the benefits of visual specification with the power of some static analysis and model checking. Some algorithms and rules are developed to permit all visual modeling constructs translated mechanically into some Promela models of AIP, as supported by the model checker SPIN. Moreover, a process is illustrated to guide the specification and verification of AIP. The method is demonstrated thoroughly using the e commerce protocol NetBill as an example.
文摘Recent development on distributed systems has shown that a variety of fairness constraints （some of which are only recently defined） play vital roles in designing self- stabilizing population protocols. Existing model checkers are deficient in verifying the systems as only limited kinds of fair- ness are supported with limited verification efficiency. In this work, we support model checking of distributed systems in the toolkit PAT （process analysis toolkit）, with a variety of fairness constraints （e.g., process-level weak/strong fairness, event-level weak/strong fairness, strong global fairness）. It performs on-the-fly verification against linear temporal prop- erties. We show through empirical evaluation （on recent pop- ulation protocols as well as benchmark systems） that PAT has advantage in model checking with fairness. Previously un- known bugs have been revealed against systems which are designed to function only with strong global fairness.
基金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.
基金The Natural Science Foundation of Jiangsu Province(No.BK2006108)
文摘Based on the authentication tests and the strand space model, the robust email protocol with perfect forward secrecy is formally analyzed, and the security shortcomings of the protocol is pointed out. Meanwhile, the man-in-the-middle attack to the protocol is given, where the attacker forges the messages in the receiving phase to cheat the two communication parties and makes them share the wrong session keys with him. Therefore, the protocol is not ensured to provide perfect forward secrecy. In order to overcome the above security shortcomings, an advanced email protocol is proposed, where the corresponding signatures in the receiving phase of the protocol are added to overcome the man-in-the-middle attack and ensure to provide perfect forward secrecy. Finally, the proposed advanced email protocol is formally analyzed with the authentication tests and the strand space model, and it is proved to be secure in authentication of the email sender, the recipient and the server. Therefore, the proposed advanced email protocol can really provide perfect forward secrecy.
文摘Exceptions are those abnormal data flow which needs additional calculation to deal with. Exception analysis concerned abnormal flow contains a lot of research content, such as exception analysis method, program verification. This article introduces another research direction of exception analysis which based on formal method. The article analyses and summarizes those research literatures referring exception analysis and exception handling logic verification based on formal reasoning and model checking. In the article, we provide an overview of the relationship and difference between traditional ideas and formal method concerning program exception analysis. In the end of the article, we make some ideas about exception analysis based on formal semantic study of procedure calls. Exception handling is seen as a special semantic effect of procedures calls.
基金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.
基金This work was supported by the French government through the UCA-Jedi project managed by the National Research Agency(ANR-15-IDEX-01)in particular,by the interdisciplinary Institute for Modeling in Neuroscience and Cognition(NeuroMod)of the UniversitéCôte d'Azur.It was also supported by the Natural Sciences and Engineering Research Council of Canada.
文摘Having a formal model of neural networks can greatly help in understanding and verifying their properties,behavior,and response to external factors such as disease and medicine.In this paper,we adopt a formal model to represent neurons,some neuronal graphs,and their composition.Some specific neuronal graphs are known for having biologically relevant structures and behaviors and we call them archetypes.These archetypes are supposed to be the basis of typical instances of neuronal information processing.In this paper we study six fundamental archetypes(simple series,series with multiple outputs,parallel composition,negative loop,inhibition of a behavior,and contralateral inhibition),and we consider two ways to couple two archetypes:(i)connecting the output(s)of the first archetype to the input(s)of the second archetype and(ii)nesting the first archetype within the second one.We report and compare two key approaches to the formal modeling and verification of the proposed neuronal archetypes and some selected couplings.The first approach exploits the synchronous programming language Lustre to encode archetypes and their couplings,and to express properties concerning their dynamic behavior.These properties are verified thanks to the use of model checkers.The second approach relies on a theorem prover,the Coq Proof Assistant,to prove dynamic properties of neurons and archetypes.
