FM
2003
Springer
13 years 9 months ago
2003
Springer
We present the formal framework for a novel approach for specifying and automatically implementing systems such as digital circuits and network protocols. The goal is to reduce the...
FM
2003
Springer
13 years 9 months ago
2003
Springer
We present ProB, an animation and model checking tool for the B method. ProB’s animation facilities allow users to gain confidence in their specifications, and unlike the anima...
FM
2003
Springer
13 years 9 months ago
2003
Springer
We present two instantiations of generic Interactive State Machines (ISMs) with mobility features which are useful for modeling and verifying dynamically changing mobile systems. I...
FM
2003
Springer
13 years 9 months ago
2003
Springer
With the steady increase in computational power of general purpose computers, our ability to analyze routine software artifacts is also steadily increasing. As a result, we are wit...
FM
2003
Springer
13 years 9 months ago
2003
Springer
Counterexamples explain why a desired temporal logic property fails to hold, and as such are considered to be the most useful form of output from model-checkers. Multi-valued model...
FM
2003
Springer
13 years 9 months ago
2003
Springer
Processor obsolescence is a serious maintenance problem for long-lived embedded control systems. A practical solution is to interpose an emulator program between the ‘legacy’ s...
FM
2003
Springer
13 years 9 months ago
2003
Springer
Abstract. Semantic Web (SW), commonly regarded as the next generation of the Web, is an emerging vision of the new Web from the Knowledge Representation and the Web communities. Th...
FM
2003
Springer
13 years 9 months ago
2003
Springer
Abstract. Program certification techniques formally show that programs satisfy certain safety policies. They rely on the correctness of the safety policy which has to be establish...
FM
2003
Springer
13 years 9 months ago
2003
Springer
We explore the question of the composition of invariance specifications in a context of concurrent and reactive systems. Depending on how compositionality is stated and how invar...
FM
2003
Springer
13 years 9 months ago
2003
Springer
A team automaton is said to satisfy compositionality if its behaviour can be described in terms of the behaviour of its constituting component automata. As an initial investigation...