Deductive Verification Method of Real-Time Safety Properties for Embedded Assembly Programs

It is important to verify both the correctness and real-time properties of embedded systems. However, as practical computer programs are represented by infinite state transition systems, specifying and verifying a computer program is difficult. Real-time properties are also important for embedded programs, but verifying the real-time properties of an embedded program is difficult. In this paper, we focus on verifying an embedded assembly program, in order to verify the real-time safety properties. We propose a deductive verification method to verify real-time safety properties, based on discrete time, as follows: (1) First, we construct a timed computational model including the execution time from the assembly program. We can specify an infinite state transition system including the execution time of the timed computational model. (2) Next, we verify whether a timed computational model satisfies RTLTL (Real-Time Linear Temporal Logic) formulas by deductive verification. We can specify real-time properties by RTLTL. By our proposed methods, we are able to achieve verification of the real-time safety properties of an embedded program.

Acting and Planning Using Operational Models

The most common representation formalisms for planning are descriptive models. They abstractly describe what the actions do and are tailored for efficiently computing the next state(s) in a state transition system. But acting requires operational models that describe how to do things, with rich control structures for closed-loop online decision-making. Using descriptive representations for planning and operational representations for acting can lead to problems with developing and verifying consistency of the different models.We define and implement an integrated acting-and-planning system in which both planning and acting use the same operational models, which are written in a general-purpose hierarchical task-oriented language offering rich control structures. The acting component is inspired by the well-known PRS system, except that instead of being purely reactive, it can get advice from the planner. Our planning algorithm, RAEplan, plans by doing Monte Carlo rollout simulations of the actor’s operational models. Our experiments show significant benefits in the efficiency of the acting and planning system.

Generic CDCL -- A Formalization of Modern Propositional Satisfiability Solvers

Modern propositional satisfiability (or SAT) solvers are very powerful due to recent developments on the underlying data structures, the used heuristics to guide the search, the deduction techniques to infer knowledge, and the formula simplification techniques that are used during pre- and inprocessing. However, when all these techniques are put together, the soundness of the combined algorithm is not guaranteed any more, and understanding the complex dependencies becomes non-trivial.In this paper we present a small set of rules that allows to model modern SAT solvers in terms of a state transition system. With these rules all techniques which are applied in modern SAT solvers can be modeled adequately. Furthermore, we show that this set of rules results is sound, complete and confluent. Finnaly, we compare the proposed transition system to related systems, and show how widely used solving techniques can be modeled.

A Formal Method of Obligation Policy for Agent Interaction

In Multi-Agent System, obligations are actions that agents are required to take or some states of affairs which should be maintained, formal modeling and verifying obligation policy which is high-level requirements specifications or communication protocol for constraining agent interaction can enhance the correctness of the system design. Therefore, in this paper a formal framework language for modeling obligation policy is introduced. In this method, the obligations are defined as a special social commitment, the state models of obligation are defined by classifying the obligation. Then we use the policy context and state model to formal the dynamic execution of obligation policy, finally the operational semantics of the framework language is defined as a state transition system which has Kripke semantic structure and it can be as formal foundation for model checking.