FAC
2008
13 years 4 months ago
2008
Given deterministic interfaces P and Q, we investigate the problem of synthesising an interface R such that P composed with R refines Q. We show that a solution exists iff P and Q ...
FAC
2008
13 years 4 months ago
2008
Abstract. Slicing is a program analysis technique that was originally introduced to improve program debugging and understanding. The purpose of a slicing algorithm is to remove the...
FAC
2008
13 years 4 months ago
2008
We extend the approach of model checking parameterized networks of processes by means of network invariants to the setting of real-time systems. We introduce timed transition stru...
FAC
2008
2008
Testing a deterministic implementation against a non-controllable non-deterministic stream X-machine
13 years 4 months ago
A stream X-machine is a type of extended finite state machine with an associated development approach that consists of building a system from a set of trusted components. One of th...
FAC
2008
13 years 4 months ago
2008
Abstract. Model checking of real-time systems against Duration Calculus (DC) specifications requires the translation of DC formulae into automata-based semantics. The existing algo...
FAC
2008
13 years 4 months ago
2008
Abstract. Bisimulations are well
FAC
2008
13 years 4 months ago
2008
Abstract. A fundamental method of analyzing a system such as a program or a circuit is invariance analysis, in which one proves that an assertion holds on all reachable states. Typ...
FAC
2008
13 years 4 months ago
2008
Substitution is fundamental to the theory of logic and computation. Is substitution something that we define on syntax on a case-by-case basis, or can we turn the idea of substitut...
FAC
2008
13 years 4 months ago
2008
Ten years ago the Mondex electronic purse was certified to ITSEC Level E6, the highest level of assuranceforsecuresystems.ThisinvolvedbuildingformalmodelsintheZnotation,linkingthem...
FAC
2008
13 years 4 months ago
2008
Abstract. In this paper we consider the relationship between refinement-oriented specification and specifications using a temporal logic. We investigate the extent to which one can...