http://www.loc.gov/mods/v3 http://www.loc.gov/standards/mods/v3/mods-3-2.xsd
Proceedings of the 1st International Conference on Integrated Formal Methods, York, 28-29 June 1999
Formal methods have been established as the rigorous engineering methodology for the system development. Applying formal methods to a large and complex system development often requires the modelling of different aspects of such a system. For instance, complex systems (such as integrated avionics systems, engine control software) can involve functional and timing requirements that must be eventually implemented as executing code on a communicating distributed topology. This book contains the papers presented at the First International Workshop on Integrated Formal Methods, held at the University of York in June 1999. The conference provided a forum for the discussion of theoretical aspects of combing behavioural and state-based formalisms and practical solutions to the industrial problems of this approach.
A Common Framework for Mixed Hardware/Software Systems -- Jifeng He -- Proof Systems for Message-Passing Process Calculi -- Matthew Hennessy -- Deductive Reasoning versus Model Checking: Two Formal Approaches for System Development -- J.N. Reed, J.E. Sinclair and F. Guigand -- Reactive System Refinement of Distributed Systems in B -- K. Lano and K. Androutsopoulos -- Specification and Refinement using a Heterogeneous Notation for Concurrency and Communication -- Richard Paige -- RT-Z: An Integration of Z and timed CSP -- Carsten Suhl -- Retrenchment and Punctured Simulation -- R. Banach and M. Poppleton -- Model-Checking CSP-OZ Specifications with FDR -- Clemens Fischer and Heike Wehreim -- A Compositional Comparison of specifications of the Alternating Bit Protocol in CCS and UNITY based on Algebra Transformation Systems -- Martin Crosse-Rhode -- Modelling Discrete Behaviour in a Continuous-Time Formalism -- Colin J. Fidge -- An Approach to the Combination of Formal Description Techniques: Statecharts and TLA -- Thomas Deiss -- Requirements for a Temporal B -- Assigning Temporal Meaning to Abstract Machines and to Abstract Systems -- Dominque Méry -- Modular Formal Specification of Data and Behaviour -- Jaco van de Pol, Jozef Hooman and Edwin de Jong -- An Object Semantic Model of an Integrated Formal Notation SOFL -- Jin Song Dong and Shaoying Liu -- Modular Verification of Dynamic Properties for reactive systems -- Jacques Julliand, P.A. Masson and H. Mountassir -- On the Refinement and Simulation of Data Types and Processes -- Christie Bolton, Jim Davies and Jim Woodcock -- The Refinement of Event Calculus Models -- Bill Stoddart and Steve Dunne -- Towards Real-Time Object-Z -- Graeme Smith and Ian Hayes -- Integration Problems in Telephone Feature Requirements -- Paul Gibson, Geoff Hamilton and Dominiqe Méry -- A Modular Framework for the Integration of Heterogeneous Notations and Tools -- Robert Büssow and Wolfgang Grieskamp -- Separating Component and Context Specification Using Promotion -- John Derrick and Eerke Boiten -- Specifying Interactive Systems in Object-Z and CSP -- Ian MacColl and David Carrington -- Overview of Semantics of TCOZ -- Brendan Mahony and Jin Song Dong -- Using a Process Algebra to Control B Operations -- Helen Treharne and Steve Schneider.
edited by Keijiro Araki, Andy Galloway, Kenji Taguchi.