Local cover image
Local cover image

FME '97, industrial applications and strengthened foundations of formal methods : 4th International Symposium of Formal Methods Europe, Graz, Austria, September 15-19, 1997 : proceedings

By: Contributor(s): Material type: TextTextSeries: Lecture notes in computer science ; 1313Publication details: Berlín : Springer, c1997Edition: 1st edDescription: xiii, 684 p. : il. ; 24 cmISBN:
  • 3540635335
Subject(s):
Contents:
Diagrams and Programming Languages for Programmable Controllers / Stuart Anderson, Konstantinos Tourlas -- Graphical Specification and Reasoning: Case Study Generalised Railroad -- Crossing / Henning Dierks, Cheryl Dietz -- A Graphic Notation for Formal Specifications of Dynamic Systems / Gianna Reggio, Mauro Larosa -- A Semantic Integration of Object-Z and CSP for the Specification of Concurrent Systems / Graeme Smith -- Class Refinement and Interface Refinement in Object-Oriented Programs / Anna Mikhajlova, Emil Sekerinski -- Formalizing Requirements for Distributed Systems with Trace Diagrams / Stephan Kleuker -- Consistent Graphical Specification of Distributed Systems / Franz Huber, Bernhard Schätz, Geralf Einert -- Design of Reactive Control Systems for Event-Driven Operations / K. Lano, A. Sanchez -- An M-Net Semantics for a Real-Time Extension of µSDL / Hans Fleischhack, Josef Tapken -- Reconciling Real-Time with Asynchronous Message Passing / M. Broy, R. Grosu, C. Klein -- Specifying the Remote Controlling of Valves in an Explosion Test Environment / Martin Schönhoff, Mojgan Kowsari -- PICGAL: Practical Use of Formal Specification to Develop a Complex Critical System / Lionel Devauchelle, Peter Gorm Larsen, Henrik Voss -- Mathematical Modeling and Analysis of an External Memory Manager / William D. Young, William R. Bevier -- Automatic Translation of VDM-SL Specifications into Gofer / Paul Mukherjee -- Towards an Integrated CASE and Theorem Proving Tool for VDM-SL / Sten Agerholm, Jacob Frost -- Specification of Required Non-determinism / K. Lano, J. Bicarregui, J. Fiadeiro, A. Lopes -- A Corrected Failure-Divergence Model for CSP in Isabelle/HOL / H. Tej, B. Wolff -- A Proof Obligation Generator for VDM-SL / Bernhard K. Aiehernig, Peter Gorm Larsen -- Verification of Cryptographic Protocols: An Experiment / Marc Mehdi Ayadi, Dominique Bolignano -- TLA + PROMELA: Conjecture, Check, Proof. Engineering New Protocols Using Methods and Formal Notations / J.-Ch. Grdgoire -- A TLA Solution to the Specification and Verification of the RLP1 Retransmission Protocol / Abdelillah Mokkedem, Michael J. Ferguson, Robert deB. Johnston -- An Efficient Technique for Deadlock Analysis of Large Scale Process Networks / J.M.R. Martin, S.A. Jassim -- Implementing a Model Checker for LEGO / Shenwei Yu, Zhaohui Luo -- Formal Verification of Transformations for Peephole Optimization / A. Dold, F.W. von Henke, H. Pfeifer, H. Rueß -- A Meta-Method for Formal Method Integration / Richard F. Paige -- Reuse of Verified Design Templates Through Extended Pattern Matching / David Hemer, Peter A. Lindsay -- A Compositional Proof System for Shared Variable Concurrency / F.S. de Boer, U. Hannemann, W.-P. de Roever -- A Framework for Modular Formal Specification and Verification / Pierre Michel, Virginie Wiels -- A Timed Semantics for the STATEMATE Implementation of Statecharts / Carsta Petersohn, Luis Urbina -- Using PVS to Prove a Z Refinement: A Case Study / David W.J. Stringer-Calvert, Susan Stepney, Ian Wand -- Verification of Reactive Systems Using DisCo and PVS / Pertti Kellomdki -- Term Rewrite Systems to Derive Set Boolean Operations on 2D Objects / David Cazier, Jean-Franfois Dufourd -- A Normal Form Reduction Strategy for Hardware/Software Partitioning / Leila Silva, Augusto Sampaio, Edna Barros -- Viewpoint Consistency in Z and LOTOS: A Case Study / Eerke Boiten, Howard Bowman, John Derrick, Maarten Steen -- A UNITY Mapping Operator for Distributed Programs / Michel Charpentier -- Author Index
Star ratings
    Average rating: 0.0 (0 votes)

ISSN 0302-9743 Incluye referencias bibliográficas e índice.

Diagrams and Programming Languages for Programmable Controllers / Stuart Anderson, Konstantinos Tourlas -- Graphical Specification and Reasoning: Case Study Generalised Railroad -- Crossing / Henning Dierks, Cheryl Dietz -- A Graphic Notation for Formal Specifications of Dynamic Systems / Gianna Reggio, Mauro Larosa -- A Semantic Integration of Object-Z and CSP for the Specification of Concurrent Systems / Graeme Smith -- Class Refinement and Interface Refinement in Object-Oriented Programs / Anna Mikhajlova, Emil Sekerinski -- Formalizing Requirements for Distributed Systems with Trace Diagrams / Stephan Kleuker -- Consistent Graphical Specification of Distributed Systems / Franz Huber, Bernhard Schätz, Geralf Einert -- Design of Reactive Control Systems for Event-Driven Operations / K. Lano, A. Sanchez -- An M-Net Semantics for a Real-Time Extension of µSDL / Hans Fleischhack, Josef Tapken -- Reconciling Real-Time with Asynchronous Message Passing / M. Broy, R. Grosu, C. Klein -- Specifying the Remote Controlling of Valves in an Explosion Test Environment / Martin Schönhoff, Mojgan Kowsari -- PICGAL: Practical Use of Formal Specification to Develop a Complex Critical System / Lionel Devauchelle, Peter Gorm Larsen, Henrik Voss -- Mathematical Modeling and Analysis of an External Memory Manager / William D. Young, William R. Bevier -- Automatic Translation of VDM-SL Specifications into Gofer / Paul Mukherjee -- Towards an Integrated CASE and Theorem Proving Tool for VDM-SL / Sten Agerholm, Jacob Frost -- Specification of Required Non-determinism / K. Lano, J. Bicarregui, J. Fiadeiro, A. Lopes -- A Corrected Failure-Divergence Model for CSP in Isabelle/HOL / H. Tej, B. Wolff -- A Proof Obligation Generator for VDM-SL / Bernhard K. Aiehernig, Peter Gorm Larsen -- Verification of Cryptographic Protocols: An Experiment / Marc Mehdi Ayadi, Dominique Bolignano -- TLA + PROMELA: Conjecture, Check, Proof. Engineering New Protocols Using Methods and Formal Notations / J.-Ch. Grdgoire -- A TLA Solution to the Specification and Verification of the RLP1 Retransmission Protocol / Abdelillah Mokkedem, Michael J. Ferguson, Robert deB. Johnston -- An Efficient Technique for Deadlock Analysis of Large Scale Process Networks / J.M.R. Martin, S.A. Jassim -- Implementing a Model Checker for LEGO / Shenwei Yu, Zhaohui Luo -- Formal Verification of Transformations for Peephole Optimization / A. Dold, F.W. von Henke, H. Pfeifer, H. Rueß -- A Meta-Method for Formal Method Integration / Richard F. Paige -- Reuse of Verified Design Templates Through Extended Pattern Matching / David Hemer, Peter A. Lindsay -- A Compositional Proof System for Shared Variable Concurrency / F.S. de Boer, U. Hannemann, W.-P. de Roever -- A Framework for Modular Formal Specification and Verification / Pierre Michel, Virginie Wiels -- A Timed Semantics for the STATEMATE Implementation of Statecharts / Carsta Petersohn, Luis Urbina -- Using PVS to Prove a Z Refinement: A Case Study / David W.J. Stringer-Calvert, Susan Stepney, Ian Wand -- Verification of Reactive Systems Using DisCo and PVS / Pertti Kellomdki -- Term Rewrite Systems to Derive Set Boolean Operations on 2D Objects / David Cazier, Jean-Franfois Dufourd -- A Normal Form Reduction Strategy for Hardware/Software Partitioning / Leila Silva, Augusto Sampaio, Edna Barros -- Viewpoint Consistency in Z and LOTOS: A Case Study / Eerke Boiten, Howard Bowman, John Derrick, Maarten Steen -- A UNITY Mapping Operator for Distributed Programs / Michel Charpentier -- Author Index

Click on an image to view it in the image viewer

Local cover image