Integrated Formal Methods: Second International Conference, IFM 2000, Dagstuhl Castle, Germany, November 1-3, 2000 Proceedings
Springer Science & Business Media, Oct 18, 2000 - Computers - 439 pages
IFM 2000, the second in a series of international conferences on Integrated F- mal Methods, was held at the 18th-century chateau DEGREES of Schloss Dagstuhl, Sa- land, Germany, from the 1st to the 3rd of November 2000. The conference programme consisted of invited talks from Sir Tony Hoare FRS and Wolfram Schulte, along with 22 papers selected from 58 submissions. Applying formal methods may involve the modelling of di erent aspects of a system that are expressed through di erent paradigms. This motivates us to research the combination of di erent viewpoints of a system, either by the creation of hybrid notations, by extending existing notations, by translating between notations, or by incorporating a wider perspective with the innovative use of an existing notation. The integration of formal methods promises great bene ts to systems - delling and software development. Regardless of the approach taken, however, signi cant issues can arise in areas such as semantic integration, the tracta- lity of our notations, the integration of tool support, the integration of proof systems, consistency, and completeness. Issues arise equally in our conceptua- sation of systems at di erent levels of abstraction and the development of these conceptualisations through the process of re nement.
What people are saying - Write a review
We haven't found any reviews in the usual places.
StateBased Extension of CASL
Linking DC Together with TRSL
Formalizing Timing Diagrams as Causal Dependencies for Verification Purposes
A Process Compensation Language
Activity Graphs and Processes
Structuring RealTime ObjectZ Speci cations
Towards Practical and Sound Interface Specifications
Construction of Finite Labelled Transition Systems from B Abstract Systems
Hows Whys and Wherefores
Combining Operational Semantics Logic Programming and Literate Programming in the Specification and Animation of the Verilog Hardware Descr...
Why Doesnt Anyone Use Formal Methods?
How to Write a Healthiness Condition
A Concurrent and Compositional Petri Net Semantics of Preemption
An Approach to Symbolic Test Generation
Behavioral Conformance Verification in an Integrated Approach Using UML and B
Cooperation of Formal Methods in an Engineering Based Software Development Process
Developing Control Systems Components
Specification and Analysis of AutomataBased Designs
Structural Refinement in ObjectZ CSP
Towards a Unified Development Methodology for SharedVariable Parallel and Distributed Programs
Other editions - View all
abstract abstract machine action activity graph algorithm allows approach automata automaton behaviour bisimulation Boolean Büchi automaton C. A. R. Hoare calculus clock compensation process components Computer Science concurrent construction control system corresponding ctr_cmd defined Deﬁnition denote described DState dynamic DynamicBag example execution expression finite Formal Methods formal techniques formula function Galois connection given healthiness condition implementation initial input interface specification IOSTS ISpec labeled transition system labelled language LNCS M-nets machine model checking modular module not-zero notation object Object-Z operational semantics output P/M-net paper parallel composition Petri nets postcondition precondition predicate diagrams process algebra Prolog properties real-time refinement refinement calculus relation rules satisfy schema sequence sequential simulation Springer-Verlag statechart diagrams StaticBag stochastic structure temporal logic Theorem trace transition system transition term translation TRSL update variables verification Verilog µ-chart