Abstract state machines, Alloy, B, VDM, and Z third international conference, ABZ 2012, Pisa, Italy, June 18-21, 2012 ; proceedings John Derrick ... (eds.)

Literaturangaben

Contribution to a Rigorous Analysis of Web Application Frameworks Egon Börger, Antonio Cisternino and Vincenzo Gervasi

Integrated Operational Semantics: Small-Step, Big-Step and Multi-step Ian J. Hayes and Robert J. Colvin

Test Generation for Sequential Nets of Abstract State Machines Paolo Arcaini, Francesco Bolis and Angelo Gargantini

ASM and Controller Synthesis Richard Banach, Huibiao Zhu, Wen Su and Xiaofeng Wu

Continuous ASM, and a Pacemaker Sensing Fragment Richard Banach, Huibiao Zhu, Wen Su and Xiaofeng Wu

An ASM Model of Concurrency in a Web Browser Vincenzo Gervasi

Modeling the Supervisory Control Theory with Alloy Benoît Fraikin, Marc Frappier and Richard St-Denis

Preventing Arithmetic Overflows in Alloy Aleksandar Milicevic and Daniel Jackson

Extending Alloy with Partial Instances Vajih Montaghami and Derek Rayside

Toward a More Complete Alloy Timothy Nelson, Daniel J. Dougherty, Kathi Fisler and Shriram Krishnamurthi

Temporal Logic Model Checking in Alloy Amirhossein Vakili and Nancy A. Day

Active Attacking Multicast Key Management Protocol Using Alloy Ting Wang and Dongyao Ji

Formalizing Hybrid Systems with Event-B Jean-Raymond Abrial, Wen Su and Huibiao Zhu

SMT Solvers for Rodin David Déharbe, Pascal Fontaine, Yoann Guyot and Laurent Voisin

Refinement Plans for Informed Formal Design Gudmund Grov, Andrew Ireland and Maria Teresa Llano

Refinement by Interface Instantiation Stefan Hallerstede and Thai Son Hoang

Discharging Proof Obligations from Atelier B Using Multiple Automated Provers David Mentré, Claude Marché, Jean-Christophe Filliâtre and Masashi Asuka

A Semantic Analysis of Logics That Cope with Partial Terms Cliff B. Jones, Matthew J. Lovert and L. Jason Steggles

Combining VDM with Executable Code Claus Ballegaard Nielsen, Kenneth Lausdahl and Peter Gorm Larsen

Extending the Test Template Framework to Deal with Axiomatic Descriptions, Quantifiers and Set Comprehensions Maximiliano Cristiá and Claudia Frydman

A Tool Chain for the Automatic Generation of Circus Specifications of Simulink Diagrams Chris Marriott, Frank Zeyda and Ana Cavalcanti

Verification of Hardware Interaction Properties of Software Ramsay Taylor

Using the Arbitrator Pattern for Dynamic Process-Instance Extension in a Work-Flow Management System Matthes Elstermann, Detlef Seese and Albert Fleischmann

A Unified Processor Model for Compiler Verification and Simulation Using ASM Roland Lezuo and Andreas Krall

Modeling Synchronization/Communication Patterns in Vision-Based Robot Control Applications Using ASMs Andrea Luzzana, Mattia Rossetti, Paolo Righettini and Patrizia Scandurra

A Reliability Prediction Method for Abstract State Machines Raffaela Mirandola, Pasqualina Potena and Patrizia Scandurra

A Simplified Parallel ASM Thesis Klaus-Dieter Schewe and Qing Wang

Refactoring Abstract State Machine Models Hamed Yaghoubi Shahir, Roozbeh Farahbod and Uwe Glässer

Continuous Behaviour in Event-B: A Sketch Richard Banach, Huibiao Zhu, Wen Su and Xiaofeng Wu

Formal Verification of PLC Programs Using the B Method Haniel Barbosa and David Déharbe

A Practical Event-B Refinement Method Based on a UML-Driven Development Process Thiago C. de Sousa, Paulo Sérgio Muniz Silva and Colin F. Snook

Learn and Test for Event-B -- A Rodin Plugin Ionut Dinca, Florentin Ipate, Laurentiu Mierla and Alin Stefanescu

Event-B Code Generation: Type Extension with Theories Andrew Edmunds, Michael Butler, Issam Maamria, Renato Silva and Chris Lovell

Formal Proofs for the NYCT Line 7 (Flushing) Modernization Project Denis Sabatier, Lilian Burdy, Antoine Requet and Jérôme Guéry

A Pattern for Modelling Fault Tolerant Systems in Event-B Gintautas Sulskus and Michael Poppleton.

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

Abstract state machines, Alloy, B, VDM, and Z

Derrick, John: Abstract State Machines, Alloy, B, VDM, and Z

Derrick, John: Abstract State Machines, Alloy, B, VDM, and Z

Archivierung/Langzeitarchivierung gewährleistet PEBW pdager DE-31