A real-time extension of ccs is described, based on true concurrency semantics and a determination to make composition the sole arbiter of real-time behaviour. The resultant calcu...
The importance of a design methodology when using Formal Description Techniques is generally agreed in the scientific community. This paper presents some design principles and con...
This paper describes a decision procedure for bisimulation-based equivalence relations between labeled transition systems. The algorithm usually performed in order to verify bisim...
A prototype Basic LOTOS interpreter, augmented for modelling real-time systems, is described. Primitive actions are treated as time-consuming, with separate start and end points, ...
Formal specifications are a well-known technique for improving software devel the context of OSI communication protocol standards, Formal Description Te (FDT's) have been dev...
Gregor von Bochmann, Daniel Ouimet, Gerald W. Neuf...
ion of LOTOS Abstract Data Types Hubert GARAVEL∗ Laboratoire de G´enie Informatique Institut I.M.A.G. GRENOBLE FRANCE This article describes an experiment with the compilation o...
Critical safety and liveness properties of a concurrent system can often be proven with the help of a reachability analysis of a finite state model. This type of analysis is usual...
The record of successful applications of formal verification techniques is slowly growing. Our ultimate aim, however, is not to perform small pilot projects that show that verific...