We discuss the projection temporal logic (PTL), based on a primitiveprojection operator, prj. A framing technique is also presented, using which a synchronizationoperator, await, is defined within the underlying logic...We discuss the projection temporal logic (PTL), based on a primitiveprojection operator, prj. A framing technique is also presented, using which a synchronizationoperator, await, is defined within the underlying logic. A framed temporal logic programminglanguage (FTLL) is presented. To illustrate how to use both the language and framing technique, someexamples are given.展开更多
A temporal logic for specifying the external behaviours of systems is introduced. Predicates INT, PASS and CLD are the primitives of the logic to record temporal states of a communication channel, i.e. intending to do...A temporal logic for specifying the external behaviours of systems is introduced. Predicates INT, PASS and CLD are the primitives of the logic to record temporal states of a communication channel, i.e. intending to do a communication, passing a message, or being closed. Auxiliary variables are recommended to describe system states by assembling channels’ states. Safety, termination, liveness and fairness can then be expressed in the logic. Specifications employing the logic will benefit from the compositionality: the conjunction of specifications of subsystems makes a specification of the whole system. Meanwhile, a CSP-like notation is suggested to specify the internal structure and the protocol of the system, called the protocol specification. A set of inference rules are also presented for proving that a system of certain protocol specification satisfies its behaviour specification. The validity of the rules is given by defining a temporal model of the CSP notation.展开更多
Atomic blocks, a high-level language construct that allows programmers to explicitly specify the atomicity of operations without worrying about the implementations, are a promising approach that simplifies concurrent ...Atomic blocks, a high-level language construct that allows programmers to explicitly specify the atomicity of operations without worrying about the implementations, are a promising approach that simplifies concurrent programming. On the other hand, temporal logic is a successful model in logic programming and concurrency verification, but none of existing temporal programming models supports concurrent programming with atomic blocks yet. In this paper, we propose a temporal programming model （αPTL） which extends the projection temporal logic （PTL） to support concurrent programming with atomic blocks. The novel construct that formulates atomic execution of code blocks, which we call atomic interval formulas, is always interpreted over two consecutive states, with the internal states of the block being abstracted away. We show that the framing mechanism in projection temporal logic also works in the new model, which consequently supports our development of an executive language. The language supports concurrency by introducing a loose interleaving semantics which tracks only the mutual exclusion between atomic blocks. We demonstrate the usage of αPTL by modeling and verifying both the fine-grained and coarse-grained concurrency.展开更多
The development of types is an important but challenging issue in temporal logic programming. In this paper, we investigate how to formalize and implement types in the temporal logic programming language MSVL, which i...The development of types is an important but challenging issue in temporal logic programming. In this paper, we investigate how to formalize and implement types in the temporal logic programming language MSVL, which is an executable subset of projection temporal logic （PTL）. Specifically, we extend MSVL with a few groups of types including basic data types, pointer types and struct types. On each type, we specify the domain of values and define some standard operations in terms of logic functions and predicates. Then, it is feasible to formalize statements of type declaration of program variables and statements of struct definitions as logic formulas. As the implementation of the theory, we extend the MSV toolkit with the support of modeling, simulation and verification of typed MSVL programs. Applications to the construction of AVL tree and ordered list show the practicality of the language.展开更多
文摘We discuss the projection temporal logic (PTL), based on a primitiveprojection operator, prj. A framing technique is also presented, using which a synchronizationoperator, await, is defined within the underlying logic. A framed temporal logic programminglanguage (FTLL) is presented. To illustrate how to use both the language and framing technique, someexamples are given.
基金Project supported by the National Natural Science Foundation of China
文摘A temporal logic for specifying the external behaviours of systems is introduced. Predicates INT, PASS and CLD are the primitives of the logic to record temporal states of a communication channel, i.e. intending to do a communication, passing a message, or being closed. Auxiliary variables are recommended to describe system states by assembling channels’ states. Safety, termination, liveness and fairness can then be expressed in the logic. Specifications employing the logic will benefit from the compositionality: the conjunction of specifications of subsystems makes a specification of the whole system. Meanwhile, a CSP-like notation is suggested to specify the internal structure and the protocol of the system, called the protocol specification. A set of inference rules are also presented for proving that a system of certain protocol specification satisfies its behaviour specification. The validity of the rules is given by defining a temporal model of the CSP notation.
基金Acknowledgements We thank for anonymous referees for their suggestions and comments. This research was based on work supported by grants from Science Foundation of China Project （60833001, 61100063, 61073040 and 61103023）, and by a Humboldt Fellowship （X.Y.） from Alexander von Humboldt Foundation.
文摘Atomic blocks, a high-level language construct that allows programmers to explicitly specify the atomicity of operations without worrying about the implementations, are a promising approach that simplifies concurrent programming. On the other hand, temporal logic is a successful model in logic programming and concurrency verification, but none of existing temporal programming models supports concurrent programming with atomic blocks yet. In this paper, we propose a temporal programming model （αPTL） which extends the projection temporal logic （PTL） to support concurrent programming with atomic blocks. The novel construct that formulates atomic execution of code blocks, which we call atomic interval formulas, is always interpreted over two consecutive states, with the internal states of the block being abstracted away. We show that the framing mechanism in projection temporal logic also works in the new model, which consequently supports our development of an executive language. The language supports concurrency by introducing a loose interleaving semantics which tracks only the mutual exclusion between atomic blocks. We demonstrate the usage of αPTL by modeling and verifying both the fine-grained and coarse-grained concurrency.
文摘The development of types is an important but challenging issue in temporal logic programming. In this paper, we investigate how to formalize and implement types in the temporal logic programming language MSVL, which is an executable subset of projection temporal logic （PTL）. Specifically, we extend MSVL with a few groups of types including basic data types, pointer types and struct types. On each type, we specify the domain of values and define some standard operations in terms of logic functions and predicates. Then, it is feasible to formalize statements of type declaration of program variables and statements of struct definitions as logic formulas. As the implementation of the theory, we extend the MSV toolkit with the support of modeling, simulation and verification of typed MSVL programs. Applications to the construction of AVL tree and ordered list show the practicality of the language.
