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 temporallogic （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.
In this article, we present a declarative propositional temporal logic programming language called TeDiLog that is a combination of the temporal and disjunctive paradigms in logicprogramming. TeDiLog is, syntacticall...
详细信息
In this article, we present a declarative propositional temporal logic programming language called TeDiLog that is a combination of the temporal and disjunctive paradigms in logicprogramming. TeDiLog is, syntactically, a sublanguage of the well-known Propositional Linear-time temporallogic (PLTL). TeDiLog allows both eventualities and always-formulas to occur in clause heads and also in clause bodies. To the best of our knowledge, TeDiLog is the first declarative temporal logic programming language that achieves this high degree of expressiveness. We establish the logical foundations of our proposal by formally defining operational and logical semantics for TeDiLog and by proving their equivalence. The operational semantics of TeDiLog relies on a restriction of the invariant-free temporal resolution procedure for PLTL that was introduced by Gaintzarain et al. in [2013]. We define a fixpoint semantics that captures the reverse (bottom-up) operational mechanism and prove its equivalence with the logical semantics. We also provide illustrative examples and comparison with other proposals.
Modeling, Simulation and Verification Language (MSVL) is a useful formalism for specification and verification of concurrent systems. To make it easy to use, we define a visual formalism, called vMSVL, which is the ex...
详细信息
ISBN:
(纸本)9783319577081;9783319577074
Modeling, Simulation and Verification Language (MSVL) is a useful formalism for specification and verification of concurrent systems. To make it easy to use, we define a visual formalism, called vMSVL, which is the extension of the classic flowchart used in software design and helps the engineer to model the structure and behaviour of a system in a visual, hierarchical way. Besides, the technique for automatical translation of vMSVL model into MSVL model is also presented. The formalism combines the benefits of the classical visualized specification method with the power of model checking, which helps to popularize the application of model checking in industry.
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, temporallogic is a successful model in logicprogramming and concurrency verification, but none of existing temporalprogramming models supports concurrent programming with atomic blocks yet. In this paper, we propose a temporalprogramming model （αPTL） which extends the projection temporallogic （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 temporallogic 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.
Modeling, Simulation and Verification Language (MSVL) is a useful formalism for specification and verification of concurrent systems. To make it more practical and easier to use, we extend MSVL with external and inter...
详细信息
Modeling, Simulation and Verification Language (MSVL) is a useful formalism for specification and verification of concurrent systems. To make it more practical and easier to use, we extend MSVL with external and internal function calls. To do so, the syntax of function definitions and function calls is formalized. Then, the syntax of expressions in MSVL is extended by including function calls. Further, the evaluation rules are redefined. Moreover, the set of statements in MSVL is also extended and the semantics of function call statements is formalized. In addition, the existence of minimal models of MSVL programs involving new added statements is proved. Finally, an example is given to illustrate how to interpret function calls in practice with MSVL. (C) 2016 Elsevier B.V. All rights reserved.
Modeling, Simulation and Verification Language (MSVL) is a useful formalism for specification and verification of concurrent systems. To make it more practical and easy to use, we extend MSVL with the technique of sem...
详细信息
ISBN:
(纸本)9783319426341;9783319426334
Modeling, Simulation and Verification Language (MSVL) is a useful formalism for specification and verification of concurrent systems. To make it more practical and easy to use, we extend MSVL with the technique of semaphore. To do so, the mechanism of MSVL function calls is deeply analyzed. Further, the semaphore type is defined. Moreover, operations over semaphore are formalized. Finally, an example is given to illustrate how to use semaphore to solve the mutual exclusion problem.
Since distributed systems are inherently concurrent and asynchronous, it is a challenge for us to verify distributed systems. MSVL is a useful temporal logic programming language and its axiomatic system has been esta...
详细信息
Since distributed systems are inherently concurrent and asynchronous, it is a challenge for us to verify distributed systems. MSVL is a useful temporal logic programming language and its axiomatic system has been established. However, the axiomatic system of MSVL lacks mechanisms to manage asynchronous communication, which makes it cannot deal with distributed systems. Thus, to verify distributed systems with MSVL in a deductive way, this paper is motivated to extend the axiomatic system of MSVL with new axioms for asynchronous communication. To this end, firstly we formalize state axioms regarding asynchronous communication commands and then prove the soundness and completeness. Further, to demonstrate how the extended axiomatic system of MSVL works for distributed systems, we apply it to the well-known Ricart-Agrawala (RA) algorithm, which is a distributed mutual exclusion algorithm and has an infinite state space. To do this, we model the RA algorithm with MSVL, specify the desired properties and then verify an instance of the RA algorithm with respect to the first-come-first-served property.
Modeling, Simulation and Verification Language (MSVL) is a useful formalism for specification and verification of concurrent systems. To make it more practical and easier to use, we extend MSVL with function calls in ...
详细信息
ISBN:
(纸本)9783319117379;9783319117362
Modeling, Simulation and Verification Language (MSVL) is a useful formalism for specification and verification of concurrent systems. To make it more practical and easier to use, we extend MSVL with function calls in this paper. To do so, an approach for function calls similar as in imperative programming languages is presented. Further, the semantics of expressions is redefined and the semantics of new added function call statements is formalized. Moreover, an example is given to illustrate how to use function calls in practice with MSVL.
A Projection temporallogic is discussed and some of its laws are given. After that, an executable temporal logic programming language, called Framed Tempura, is formalized. A minimal model-based approach for framing ...
详细信息
A Projection temporallogic is discussed and some of its laws are given. After that, an executable temporal logic programming language, called Framed Tempura, is formalized. A minimal model-based approach for framing in temporal logic programming is presented. Since framing destroys monotonicity, canonical models - used to define the semantics of non-framed programs - are no longer appropriate. To deal with this, a minimal model theory is developed, using which the temporal semantics of framed programs is captured. The existence of a minimal model for a given framed program is demonstrated. A synchronous communication mechanism for concurrent programs is provided by means of the framing technique and minimal model semantics. (C) 2007 Elsevier B.V. All rights reserved.
In this paper, an extended projection temporallogic(EPTL), based on a primitive operator prj, is formalized. Further, as an executable subset of EPTL, an object-oriented MSVL is presented, which extends the temporal ...
详细信息
ISBN:
(纸本)9780819490254
In this paper, an extended projection temporallogic(EPTL), based on a primitive operator prj, is formalized. Further, as an executable subset of EPTL, an object-oriented MSVL is presented, which extends the temporal logic programming language MSVL to support object, class, aliasing, inheritance and overloading features. An example of modeling and simulating digital signal processing is given to illustrate how to use and execute the language.
暂无评论