Electronic Notes in Theoretical Computer Science (ENTCS)

This paper presents a case study in formal software development of a plugin for a Java Desktop project management application using JML. Our goals for the case study include determining how JML-based formal methods can be incorporated in traditional ...

The Matlab Simulink tool is widely used to construct and analyse control law diagrams. Many have worked on techniques to enhance analysis facilities, and previously, we have considered the complementary problem of proving correctness of implementations ...

Graph grammars are a formal description technique suitable for the specification of distributed and reactive systems. Model-checking of graph grammars is currently supported by various approaches. However, in many situations the use of this technique ...

Java Card is a version of Java developed to run on devices with severe storage and processing restrictions. The applets that run on these devices are frequently intended for use in critical, highly distributed, mobile conditions. They are required to be ...

This paper investigates the application of the B method beyond the classical algorithmic level provided by the B0 sub-language, and presents refinements of B models at a level of precision equivalent to assembly language. We claim and justify that this ...

During a program's execution, state information can be collected and stored in the form of program traces. With such traces, one can analyze dynamic properties of the program. In this paper, we consider the problem of merging multiple traces from the ...

SMT (Satisfiability Modulo Theories) solvers are automatic verification engines suitable to discharge important classes of proof obligations generated in applying formal construction of software and hardware designs. In this paper, we present a new ...

Data refinement is useful in software development because it allows one to build more concrete specifications from abstract ones, as long as there is a mathematical relation between them. It has associated rules (proof obligations) that must be ...

We propose an extension to Message Sequence Charts (MSC); MSC diagrams comprise processes (called instances) and messages. Messages in MSC are either asynchronous or method calls. Our extension adds multiple synchronous messages. We present a ...

This paper addresses the problem of model-based off-line selection of test cases for testing the conformance of a black-box implementation with respect to a specification, in the context of reactive systems. Efficient solutions to this problem have been ...

This paper presents a new proof-assistant based approach to program verification: programs are translated, via fully-automatic deduction, into tail-recursive function defined in the logic of a theorem prover. This approach improves on well-established ...

The compilation of Handel-C programs into net-list descriptions of hardware components has been extensively used in commercial tools but never formally verified. In this paper, we first introduce a variation of the existing semantic model for Handel-C ...

We describe the formal specification and verification of a new fault-tolerant real-time communication protocol, called DoRiS, which is designed for supporting distributed real-time systems that use a shared high-bandwidth medium. Since such a kind of ...

In this paper we present a semantic embedding of Hoare and He's Unifying Theories of Programming (UTP) framework into the ProofPower-Z theorem prover; it concisely captures the notion of UTP theory, theory instantiation, and, additionally, type ...