Proceedings of the 1st International Conference on Integrated Formal Methods, York, 28-29 June 1999
Buch, Englisch, 477 Seiten, Format (B × H): 155 mm x 235 mm, Gewicht: 744 g
ISBN: 978-1-85233-107-8
Verlag: Springer
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.
Zielgruppe
Research
Autoren/Hrsg.
Fachgebiete
Weitere Infos & Material
Invited Talks.- A Common Framework for Mixed Hardware/Software Systems.- Proof Systems for Message-Passing Process Calculi (abstract only).- Z/Object-Z + CSP + Real Time.- RT-Z: An Integration of Z and timed CSP.- Towards Real-Time Object-Z.- Overview of the Semantics of TCOZ.- Temporal Logic.- Modular Verification of Dynamic Properties for Reactive Systems.- Modular Formal Specification of Data and Behaviour.- Integration Problems in Telephone Feature Requirements.- Z/Object Z + Behaviour 1.- The Refinement of Event Calculus Models.- Modelling Discrete Behaviour in a Continuous-Time Formalism.- An Object Semantic Model of SOFL.- State Charts.- A Modular Framework for the Integration of Heterogeneous Notations and Tools.- An Approach to the Combination of Formal Description Techniques:State charts and TLA.- Semantic Models & Refinement.- A Compositional Comparison of Specifications of the Alternating Bit Protocol in CCS and UNITY Based on Algebra Transformation Systems.- On the Refmement and Simulation of Data Types and Processes.- Specifying Component and Context Specification Using Promotion.- Z/Object Z + Behaviour 2.- Model-Checking CSP-OZ Specifications with FDR.- Specifying Interactive Systems in Object-Z and CSP.- Specification and Refinement using a Heterogeneous Notation for Concurrency and Communication.- (Abstract + Action) Systems.- Deductive Reasoning versus Model Checking: Two Formal Approaches for System Development.- Requirements for a Temporal B - Assigning Temporal Meaning to Abstract Machines. and to Abstract Systems.- Reactive System Refinement of Distributed Systems in B.- The B Method: Behaviour and Retrenchment.- Using a Process Algebra to Control B OPERATIONS.- Retrenchment and Punctured Simulation.- Author Index.
