ZB 2003 : formal specification and development in Z and B : third International Conference of B and Z Users, Turku, Finland, June 4-6, 2003 : proceedings

書誌事項

ZB 2003 : formal specification and development in Z and B : third International Conference of B and Z Users, Turku, Finland, June 4-6, 2003 : proceedings

Didier Bert ... [et al.] (eds.)

(Lecture notes in computer science, 2651)

Springer, c2003

大学図書館所蔵 件 / 21

この図書・雑誌をさがす

注記

Includes bibliographical references and index

Other editors: Jonathan P. Bowen, Steve King, Marina Waldén

内容説明・目次

内容説明

The refereed proceedings of the Third International Conference of Z and B Users, ZB 2003, held in Turku, Finland in June 2003. The 28 revised full papers presented together with 3 invited papers were carefully reviewed and selected for inclusion in the book. The book documents the recent advances for the Z formal specification notation and for the B method, spanning the full scope from foundational, theoretical, and methodological issues to advanced applications, tools, and case studies.

目次

Alloy: A Logical Modelling Language.- An Outline Pattern Language for Z: Five Illustrations and Two Tables.- Patterns to Guide Practical Refactoring: Examples Targetting Promotion in Z.- Reuse of Specification Patterns with the B Method.- Composing Specifications Using Communication.- When Concurrent Control Meets Functional Requirements, or Z + Petri-Nets.- How to Diagnose a Modern Car with a Formal B Model?.- Parallel Hardware Design in B.- Operation Refinement and Monotonicity in the Schema Calculus.- Using Coupled Simulations in Non-atomic Refinement.- An Analysis of Forward Simulation Data Refinement.- B#: Toward a Synthesis between Z and B.- Introducing Backward Refinement into B.- Expression Transformers in B-GSL.- Probabilistic Termination in B.- Probabilistic Invariants for Probabilistic Machines.- Proving Temporal Properties of Z Specifications Using Abstraction.- Compositional Verification for Object-Z.- Timed CSP and Object-Z.- Object Orientation without Extending Z.- Comparison of Formalisation Approaches of UML Class Constructs in Z and Object-Z.- Towards Practical Proofs of Class Correctness.- Automatically Generating Information from a Z Specification to Support the Classification Tree Method.- Refinement Preserves PLTL Properties.- Proving Event Ordering Properties for Information Systems.- ZML: XML Support for Standard Z.- Formal Derivation of Spanning Trees Algorithms.- Using B Refinement to Analyse Compensating Business Processes.- A Formal Specification in B of a Medical Decision Support System.- Extending B with Control Flow Breaks.- Towards Dynamic Population Management of Abstract Machines in the B Method.

「Nielsen BookData」 より

関連文献: 1件中  1-1を表示

詳細情報

ページトップへ