Refinement serves as a crucial link in software engineering, transforming abstract descriptions of systems into practical implementations. This process bridges the gap between high-level requirements and their execution, ensuring that theoretical concepts are effectively translated into functional software or hardware solutions. The book delves into the methodologies and principles of refinement, highlighting its importance in achieving precise and reliable system design.
This book constitutes the proceedings of the Third International Conference on Abstract State Machines, B, VDM, and Z, which took place in Pisa, Italy, in June 2012. The 20 full papers presented together with 2 invited talks and 13 short papers were carefully reviewed and selected from 59 submissions. The ABZ conference series is dedicated to the cross-fertilization of five related state-based and machine-based formal methods: Abstract State Machines (ASM), Alloy, B, VDM, and Z. They share a common conceptual foundation and are widely used in both academia and industry for the design and analysis of hardware and software systems. The main goal of this conference series is to contribute to the integration of these formal methods, clarifying their commonalities and differences to better understand how to combine different approaches for accomplishing the various tasks in modeling, experimental validation and mathematical verification of reliable high-quality hardware/software systems.
This book constitutes the refereed proceedings of the 9th International Conference on Integrated Formal Methods, IFM 2012, held Pisa, Italy, in June 2012. The 20 revised full papers presented together with 2 invited papers were carefully reviewed and selected from 59 submissions. The papers cover the spectrum of integrated formal methods, ranging from formal and semiformal notations, semantics, proof frameworks, refinement, verification, timed systems, as well as tools and case studies.
These proceedings feature papers from the 27th FORTE conference, which focuses on Formal Techniques for Networked and Distributed Systems. This international annual event combines the former PSTV (Protocol Specification Testing and Verification) and FORTE (Formal Description Techniques for Distributed Systems and Communication Protocols) conferences, with PSTV's inaugural meeting in 1981 and FORTE's in 1988. The two conferences merged in 1996 and have been known as FORTE since 2001. The conference serves as a platform for discussing advancements in theory, applications, tools, and the industrialization of formal methods. Over the years, FORTE has taken place in various locations, including Pisa, Cheju Island, Houston, Berlin, Madrid, Paris, Taiwan, and most recently, Tallinn, Estonia. Sponsored by Working Group 6.1 of Technical Committee 6 (TC6) of the International Federation for Information Processing (IFIP), FORTE is a flagship event for WG6.1, addressing key themes such as formal description techniques, open distributed systems, and quality of service. WG6.1 also provided a Best Paper Award and funding to support student participation. The 27th conference occurred from June 26–29, 2007, in the historical Brotherhood of the Black Heads building in Tallinn.
Refinement is one of the cornerstones of the formal approach to software engineering, and its use in various domains has led to research on new applications and generalisation. This book brings together this important research in one volume, with the addition of examples drawn from different application areas. It covers four main - data refinement and its application to Z; - generalisations of refinement that change the interface and atomicity of operations; - refinement in Object-Z; - and modelling state and behaviour by combining Object-Z with CSP. Refinement in Z and Foundations and Advanced Applications provides an invaluable overview of recent research for academic and industrial researchers, lecturers teaching formal specification and development, industrial practitioners using formal methods in their work, and postgraduate and advanced undergraduate students.