Sciweavers

Share
FM
2003
Springer
107views Formal Methods» more  FM 2003»
10 years 3 months ago
A Formal Framework for Modular Synchronous System Design
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...
Maria-Cristina V. Marinescu, Martin C. Rinard
FM
2003
Springer
114views Formal Methods» more  FM 2003»
10 years 3 months ago
ProB: A Model Checker for B
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...
Michael Leuschel, Michael J. Butler
FM
2003
Springer
146views Formal Methods» more  FM 2003»
10 years 3 months ago
Interacting State Machines for Mobility
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...
Thomas A. Kuhn, David von Oheimb
FM
2003
Springer
129views Formal Methods» more  FM 2003»
10 years 3 months ago
Trends in Software Verification
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...
Gerard J. Holzmann
FM
2003
Springer
98views Formal Methods» more  FM 2003»
10 years 3 months ago
Generating Counterexamples for Multi-valued Model-Checking
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...
Arie Gurfinkel, Marsha Chechik
FM
2003
Springer
107views Formal Methods» more  FM 2003»
10 years 3 months ago
Verifying Emulation of Legacy Mission Computer Systems
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...
Colin J. Fidge
FM
2003
Springer
169views Formal Methods» more  FM 2003»
10 years 3 months ago
Checking and Reasoning about Semantic Web through Alloy
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...
Jin Song Dong, Jing Sun, Hai H. Wang
FM
2003
Springer
108views Formal Methods» more  FM 2003»
10 years 3 months ago
Correctness of Source-Level Safety Policies
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...
Ewen Denney, Bernd Fischer 0002
FM
2003
Springer
92views Formal Methods» more  FM 2003»
10 years 3 months ago
Composing Invariants
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...
Michel Charpentier
FM
2003
Springer
89views Formal Methods» more  FM 2003»
10 years 3 months ago
Team Automata Satisfying Compositionality
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...
Maurice H. ter Beek, Jetty Kleijn
books