Abstract state machines, Alloy, B, TLA, VDM, and Z : 5th International Conference, ABZ 2016, Linz, Austria, May 23-27, 2016, Proceedings /: 5th International Conference, ABZ 2016, Linz, Austria, May 23-27, 2016, Proceedings. (2016)

• Record Type: Book
• Other Titles: ABZ 2016
• Further Information: Note: Michael Butler, Klaus-Dieter Schewe, Atif Mashkoor, Miklos Biro (eds.).
• Editors: Butler, Michael; Schewe, Klaus-Dieter; Mashkoor, Atif; Biro, Mikloš
• Other Names: ABZ (Conference), 5th
• Contents: Modeling Distributed Algorithms by Abstract State Machines Compared to Petri Nets -- A Universal Control Construct for Abstract State Machines -- Encoding TLA+ into Many-Sorted First-Order Logic -- Proving Determinacy of PharOS in TLA+ -- A Rigorous Correctness Proof for Pastry -- Enabling Analysis for B and Event-B -- A Compact Encoding of Sequential ASMs in Event-B -- Proof Assisted Symbolic Model Checking for B and Event-B -- On Component-based Reuse for Event-B -- Using B and ProB for Data Validation Projects -- Generating Event-B Specifications from Algorithm Descriptions -- Formal Proofs of Termination Detection for Local Computations by Refinement-Based Compositions -- How to Select the Suitable Formal Method for an Industrial Application: A Survey -- Unified Syntax for Abstract State Machines -- A Relational Encoding for a Clash-Free Subset of ASMs -- Towards an ASM Thesis for Reflective Sequential Algorithms -- A Model-based Transformation Approach to Reuse and Retarget CASM Specifications -- Modeling a Discrete Wet-Dry Algorithm for Hurricane Storm Surge in Alloy -- `The Tinker' for Rodin -- A Graphical Tool for Event Refinement Structures in Event-B -- Rodin Platform Why3 plug-in -- Semi-Automated Design Space Exploration for Formal Modelling -- Handling Continuous Functions in Hybrid Systems Reconfigurations: A Formal Event-B Development -- UC-B: Use Case Modelling with Event-B -- Interactive Model Repair by Synthesis -- SysML2B: Automatic Tool for B Project Graphical Architecture Design using SysML -- Mechanized Refinement of Communication Models with TLA+ -- A Super Industrial Application of PSGraph -- The Hemodialysis Machine Case Study -- How to Assure Correctness and Safety of Medical Software: The Hemodialysis Machine Case Study -- Validating the Requirements and Design of a Hemodialysis Machine Using iUML-B, BMotionStudio, and Co-simulation -- Hemodialysis Machine in Hybrid Event-B -- Modeling a Hemodialysis Machine using Algebraic State-Transition Diagrams and B-like Methods -- Modelling the Haemodialysis Machine with Circus.
• Publisher Details: Switzerland : Springer
• Publication Date: 2016
• Extent: 1 online resource (xxi, 426 pages), illustrations
• Subjects: 006.3/1; Computer science; Machine learning -- Congresses; Machine theory -- Congresses; Logic design; Software engineering; Machine learning; Machine theory; Computers -- Programming -- General; Computers -- Machine Theory; Computers -- Software Development & Engineering -- General; Computers -- Programming Languages -- General; Computer programming / software development; User interface design & usability; Software Engineering; Programming & scripting languages: general; Mathematics -- Logic; Mathematical theory of computation; Electronic books; Conference papers and proceedings; Electronic books
• Languages: English
• ISBNs: 9783319336008; 3319336002; 3319335995; 9783319335995
• Related ISBNs: 9783319335995
• Notes: Note: Online resource; title from PDF title page (SpringerLink, viewed May 18, 2016).
• Access Rights: Legal Deposit; Only available on premises controlled by the deposit library and to one user at any one time; The Legal Deposit Libraries (Non-Print Works) Regulations (UK).
• Access Usage: Restricted: Printing from this resource is governed by The Legal Deposit Libraries (Non-Print Works) Regulations (UK) and UK copyright law currently in force.