Integrated Formal Methods

Second International Conference, IFM 2000, Dagstuhl Castle, Germany, November 1-3, 2000 Proceedings

Wolfgang Grieskamp, Thomas Santen, Bill Stoddart (Herausgeber)

Buch | Softcover

X, 446 Seiten

2000
Springer Berlin (Verlag)
978-3-540-41196-3 (ISBN)

Artikel merken

IFM 2000, the second in a series of international conferences on Integrated F- mal Methods, was held at the 18th-century chateau ^ 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.

Invited Talk.- Assertions.- Linking and Extending Notations.- State-Based 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 Real-Time Object-Z Specifications.- ISpec: Towards Practical and Sound Interface Specifications.- Methodology.- Cooperation of Formal Methods in an Engineering Based Software Development Process.- Developing Control Systems Components.- Specification and Analysis of Automata-Based Designs.- Structural Refinement in Object-Z / CSP.- Towards a Unified Development Methodology for Shared-Variable Parallel and Distributed Programs.- Foundation of One Formalism by Another.- Construction of Finite Labelled Transition Systems from B Abstract Systems.- ?-Charts and Z: Hows, Whys, and Wherefores.- Combining Operational Semantics, Logic Programming and Literate Programming in the Specification and Animation of the Verilog Hardware Description Language.- Invited Talk.- Why Doesn't Anyone Use Formal Methods?.- Semantics.- How to Write a Healthiness Condition.- A Concurrent and Compositional Petri Net Semantics of Preemption.- Verification and Validation.- An Approach to Symbolic Test Generation.- Behavioral Conformance Verification in an Integrated Approach Using UML and B.- Predicate Diagrams for the Verification of Reactive Systems.- Modular Verification for a Class of PLTL Properties.- Towards Model Checking Stochastic Process Algebra.

Erscheint lt. Verlag	18.10.2000
Reihe/Serie	Lecture Notes in Computer Science
Zusatzinfo	X, 446 p.
Verlagsort	Berlin
Sprache	englisch
Maße	155 x 235 mm
Gewicht	635 g
Themenwelt	Mathematik / Informatik ► Informatik ► Programmiersprachen / -werkzeuge
	Mathematik / Informatik ► Informatik ► Software Entwicklung
	Mathematik / Informatik ► Informatik ► Theorie / Studium
Schlagworte	Formalisierung • Formal Method • formal methods • Formal Notations • formal specification • Formal Validation • Formal Verification • Hardcover, Softcover / Informatik, EDV/Informatik • HC/Informatik, EDV/Informatik • Mathematics of Program Construction • program analysis • Programmic Logics • Program Semantics • Reactive Systems • Semantics • Software Refinement • Validation • verification
ISBN-10	3-540-41196-8 / 3540411968
ISBN-13	978-3-540-41196-3 / 9783540411963
Zustand	Neuware