Coverart for item
The Resource Abstract state machines, Alloy, B, VDM, and Z : third International Conference, ABZ 2012, Pisa, Italy, June 18-21, 2012. Proceedings, John Derrick [and others] (eds.), (electronic resource)

Abstract state machines, Alloy, B, VDM, and Z : third International Conference, ABZ 2012, Pisa, Italy, June 18-21, 2012. Proceedings, John Derrick [and others] (eds.), (electronic resource)

Label
Abstract state machines, Alloy, B, VDM, and Z : third International Conference, ABZ 2012, Pisa, Italy, June 18-21, 2012. Proceedings
Title
Abstract state machines, Alloy, B, VDM, and Z
Title remainder
third International Conference, ABZ 2012, Pisa, Italy, June 18-21, 2012. Proceedings
Statement of responsibility
John Derrick [and others] (eds.)
Title variation
ABZ 2012
Creator
Contributor
Subject
Genre
Language
eng
Summary
  • 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 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
  • Annotation:
Member of
Cataloging source
TXU
Dewey number
006.3/1
LC call number
Q325.5
LC item number
.A29 2012
http://bibfra.me/vocab/lite/meetingDate
2012
http://bibfra.me/vocab/lite/meetingName
ABZ (Conference)
http://library.link/vocab/relatedWorkOrContributorDate
1963-
http://library.link/vocab/relatedWorkOrContributorName
Derrick, John
Series statement
  • Lecture notes in computer science,
  • LNCS sublibrary. SL 1, Theoretical computer science and general issues
Series volume
7316
http://library.link/vocab/subjectName
  • Machine learning
  • Formal methods (Computer science)
Summary expansion
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
Label
Abstract state machines, Alloy, B, VDM, and Z : third International Conference, ABZ 2012, Pisa, Italy, June 18-21, 2012. Proceedings, John Derrick [and others] (eds.), (electronic resource)
Instantiates
Publication
Note
International conference proceedings
Bibliography note
Includes bibliographical references and author index
Contents
  • 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
  • Contribution to a Rigorous Analysis of Web Application Frameworks
  • 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
  • Egon Börger, Antonio Cisternino and Vincenzo Gervasi
  • 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
  • Integrated Operational Semantics: Small-Step, Big-Step and Multi-step
  • 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
  • Ian J. Hayes and Robert J. Colvin
  • 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
  • Test Generation for Sequential Nets of Abstract State Machines
  • 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
  • Paolo Arcaini, Francesco Bolis and Angelo Gargantini
  • A Pattern for Modelling Fault Tolerant Systems in Event-B
  • Gintautas Sulskus and Michael Poppleton
  • 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
  • Contribution to a Rigorous Analysis of Web Application Frameworks
  • 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
  • Egon Börger, Antonio Cisternino and Vincenzo Gervasi
  • 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
  • Integrated Operational Semantics: Small-Step, Big-Step and Multi-step
  • 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
  • Ian J. Hayes and Robert J. Colvin
  • 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
  • Test Generation for Sequential Nets of Abstract State Machines
  • 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
  • Paolo Arcaini, Francesco Bolis and Angelo Gargantini
  • A Pattern for Modelling Fault Tolerant Systems in Event-B
  • Gintautas Sulskus and Michael Poppleton
  • ASM and Controller Synthesis
  • Richard Banach, Huibiao Zhu, Wen Su and Xiaofeng Wu
Control code
OCM1bookssj0000697433
Dimensions
unknown
Isbn
9783642308840
Lccn
2016301945
Other control number
10.1007/978-3-642-30885-7
Specific material designation
remote
System control number
(WaSeSS)bookssj0000697433
Label
Abstract state machines, Alloy, B, VDM, and Z : third International Conference, ABZ 2012, Pisa, Italy, June 18-21, 2012. Proceedings, John Derrick [and others] (eds.), (electronic resource)
Publication
Note
International conference proceedings
Bibliography note
Includes bibliographical references and author index
Contents
  • 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
  • Contribution to a Rigorous Analysis of Web Application Frameworks
  • 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
  • Egon Börger, Antonio Cisternino and Vincenzo Gervasi
  • 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
  • Integrated Operational Semantics: Small-Step, Big-Step and Multi-step
  • 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
  • Ian J. Hayes and Robert J. Colvin
  • 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
  • Test Generation for Sequential Nets of Abstract State Machines
  • 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
  • Paolo Arcaini, Francesco Bolis and Angelo Gargantini
  • A Pattern for Modelling Fault Tolerant Systems in Event-B
  • Gintautas Sulskus and Michael Poppleton
  • 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
  • Contribution to a Rigorous Analysis of Web Application Frameworks
  • 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
  • Egon Börger, Antonio Cisternino and Vincenzo Gervasi
  • 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
  • Integrated Operational Semantics: Small-Step, Big-Step and Multi-step
  • 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
  • Ian J. Hayes and Robert J. Colvin
  • 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
  • Test Generation for Sequential Nets of Abstract State Machines
  • 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
  • Paolo Arcaini, Francesco Bolis and Angelo Gargantini
  • A Pattern for Modelling Fault Tolerant Systems in Event-B
  • Gintautas Sulskus and Michael Poppleton
  • ASM and Controller Synthesis
  • Richard Banach, Huibiao Zhu, Wen Su and Xiaofeng Wu
Control code
OCM1bookssj0000697433
Dimensions
unknown
Isbn
9783642308840
Lccn
2016301945
Other control number
10.1007/978-3-642-30885-7
Specific material designation
remote
System control number
(WaSeSS)bookssj0000697433

Library Locations

    • Ellis LibraryBorrow it
      1020 Lowry Street, Columbia, MO, 65201, US
      38.944491 -92.326012
    • Engineering Library & Technology CommonsBorrow it
      W2001 Lafferre Hall, Columbia, MO, 65211, US
      38.946102 -92.330125
Processing Feedback ...