Fundamenta Informaticae - Volume 70, issue 1-2

Authors: Janicki, Ryszard

Article Type: Other

Citation: Fundamenta Informaticae, vol. 70, no. 1-2, pp. v-vi, 2006

Authors: Björklund, Dag | Lilius, Johan

Article Type: Research Article

Abstract: The B method is one of the few formal methods with commerciallly available tool support. It has been succesfully applied in the development of several industrial applications. In this paper we present an application of the B-Method to a new domain, namely language development. We have developed an approach for translating a language with a structural operational semantics into B specifications. The language semantics is specified in separate B machines, that act as an interpreter for …programs in the language. The programs, represented as abstract syntax trees, can then automatically be translated into B specifications. We have used the approach in the context of Rialto, a language for multiple models of computation. We show how Rialto programs are translated into B machines, and how the different scheduling policies that are used to interpret concurrency can be also be represented as B machines. We also discuss some shortcomings of the approach and the B-Tools that we have available. Show more

Citation: Fundamenta Informaticae, vol. 70, no. 1-2, pp. 1-20, 2006

Authors: Kapoor, Hemangee K. | Josephs, Mark B. | Furey, Dennis P.

Article Type: Research Article

Abstract: A delay-insensitive module communicates with its environment through wires of unbounded delay. To avoid transmission interference, the absorption of a signal transition must be acknowledged before another one is propagated along the same wire. The environment may guarantee, however, to interact with the module in an even more restrictive way. It is worthwhile taking this into account when synthesising the module because it may allow for a cheaper, faster implementation. The concept of restriction has been …built into our translation tool, di2pn (to help in synthesis), and our analysis tool, diana (to perform equivalence and refinement checking). Formally, DI-Algebra is equipped with a new operator that weakens the specification of a module by taking its environment into account. This operator is a useful instance of divergence extension, a concept introduced by Mallon. Divergence extension in general, and restriction and alternation in particular, can be represented with the parallel composition operator and so are amenable to algebraic reasoning. Show more

Keywords: Delay-insensitivity, Verification, Process algebra, Restrictive environments, Closed systems, Asynchronous circuits

Citation: Fundamenta Informaticae, vol. 70, no. 1-2, pp. 21-48, 2006

Authors: Khomenko, Victor | Koutny, Maciej | Yakovlev, Alex

Article Type: Research Article

Abstract: The behaviour of asynchronous circuits is often described by Signal Transition Graphs (STGs), which are Petri nets whose transitions are interpreted as rising and falling edges of signals. One of the crucial problems in the synthesis of such circuits is deriving equations for logic gates implementing each output signal of the circuit. This is usually done using reachability graphs. In this paper, we avoid constructing the reachability graph of an STG, which can lead …to state space explosion, and instead use only the information about causality and structural conflicts between the events involved in a finite and complete prefix of its unfolding. We propose an efficient algorithm for logic synthesis based on the Incremental Boolean Satisfiability (SAT) approach. Experimental results show that this technique leads not only to huge memory savings when compared with the methods based on reachability graphs, but also to significant speedups in many cases, without affecting the quality of the solution. Show more

Keywords: logic synthesis, automated synthesis, asynchronous circuits, self-timed circuits, Petrinets, signal transition graphs, STG, incremental SAT, net unfoldings, partial order techniques

Citation: Fundamenta Informaticae, vol. 70, no. 1-2, pp. 49-73, 2006

Authors: Lawford, Mark | Pantelic, Vera | Zhang, Hong

Article Type: Research Article

Abstract: This paper describes an attempt to combine theorem proving and model-checking to formally verify real-time systems in a discrete time setting. The Timed Automata Modeling Environment (TAME) has been modified to provide a formal model for Time Transition Models (TTMs) in the PVS proof checker. Strong and weak state-event observation equivalences are formalized in PVS for state-event labeled transition systems (SELTS), the underlying semantic model of TTMs. The state-event equivalences form the basis of truth value …preserving abstractions for a real-time temporal logic. When appropriate restrictions are placed upon the TTMs, their PVS models can be easily translated into input for the SAL model-checker. A simple real-time control system is specified and verified using these theories. While these preliminary results indicate that the combination of PVS and SAL could provide a useful environment to perform equivalence verification, model-checking and compositional model reduction of real-time systems, the current implementation in the general purpose SAL model-checker lags well behind state of the art real-time model-checkers. Show more

Keywords: Real-time, equivalence verification, theorem proving, PVS, model-checking, model reduction, SAL

Citation: Fundamenta Informaticae, vol. 70, no. 1-2, pp. 75-110, 2006

Authors: Seppi, Kevin | Jones, Michael | Lamborn, Peter

Article Type: Research Article

Abstract: This paper presents a meta-heuristic for use in finding errors in models of complex concurrent systems using explicit guided model checking. The meta-heuristic improves explicit guided model checking by applying the empirical Bayes method to revise heuristic estimates of the distance from a given state to an error state. Guided search using the revised estimates finds errors with less search effort than the original estimates.

Citation: Fundamenta Informaticae, vol. 70, no. 1-2, pp. 111-126, 2006

Authors: Tauriainen, Heikki

Article Type: Research Article

Abstract: We generalize the classic explicit-state emptiness checking algorithm for Büchi word automata (the nested depth-first search) into Büchi automata with multiple acceptance conditions. Avoiding a degeneralization step improves the algorithm's worst-case memory requirements and reduces the worst-case number of state visits during the search. We give experimental results and discuss changes needed to make the generalized algorithmcompatible with well-known probabilistic explicit-state model checking techniques.

Keywords: Model checking, uchi automata, nested depth-first search

Citation: Fundamenta Informaticae, vol. 70, no. 1-2, pp. 127-154, 2006

Authors: Xia, Fei | Hao, Fei | Clark, Ian | Yakovlev, Alex | Chester, E. Graeme

Article Type: Research Article

Abstract: Previous work on asynchronous communication mechanisms (ACMs) has not dealt with buffered forms (with the number of data cells n>1). This paper describes a systematic design/synthesis process for ACMs with arbitrary buffer size, a series of resulting buffered ACM algorithms, and the modelling and simulation of these ACMs using Matlab, putting ACMs (esp. buffered ones) in the context of complex engineering systems.

Citation: Fundamenta Informaticae, vol. 70, no. 1-2, pp. 155-170, 2006