Michael J. Butler
According to our database1,
Michael J. Butler
authored at least 144 papers
between 1990 and 2018.
Collaborative distances:
Collaborative distances:
Timeline
Legend:
Book In proceedings Article PhD thesis OtherLinks
Homepages:
-
at zbmath.org
-
at orcid.org
-
at dl.acm.org
On csauthors.net:
Bibliography
2018
Validating and verifying the requirements and design of a haemodialysis machine using the Rodin toolset.
Sci. Comput. Program., 2018
Introduction to the ABZ 2016 Special issue.
Sci. Comput. Program., 2018
A model-based framework for software portability and verification in embedded power management systems.
Journal of Systems Architecture - Embedded Systems Design, 2018
Developing A New Language to Construct Algebraic Hierarchies for Event-B.
Proceedings of the Dependable Software Engineering. Theories, Tools, and Applications, 2018
Refinement of Timing Constraints for Concurrent Tasks with Scheduling.
Proceedings of the Abstract State Machines, Alloy, B, TLA, VDM, and Z, 2018
The Hybrid ERTMS/ETCS Level 3 Case Study.
Proceedings of the Abstract State Machines, Alloy, B, TLA, VDM, and Z, 2018
Verifiable Code Generation from Scheduled Event-B Models.
Proceedings of the Abstract State Machines, Alloy, B, TLA, VDM, and Z, 2018
2017
Derivation of algorithmic control structures in Event-B refinement.
Sci. Comput. Program., 2017
Core Hybrid Event-B II: Multiple cooperating Hybrid Event-B machines.
Sci. Comput. Program., 2017
Incremental Database Design using UML-B and Event-B.
Proceedings of the Proceedings Joint Workshop on Handling IMPlicit and EXplicit knowledge in formal system development (IMPEX) and Formal and Model-Driven Techniques for Developing Trustworthy Systems (FM&MDD), 2017
Theory Plug-in for Rodin 3.x.
CoRR, 2017
Formal Modelling Techniques for Efficient Development of Railway Control Products.
Proceedings of the Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification, 2017
Analysing Security Protocols Using Refinement in iUML-B.
Proceedings of the NASA Formal Methods - 9th International Symposium, 2017
Formal Development of Policing Functions for Intelligent Systems.
Proceedings of the 28th IEEE International Symposium on Software Reliability Engineering, 2017
Class-Diagrams for Abstract Data Types.
Proceedings of the Theoretical Aspects of Computing - ICTAC 2017, 2017
A Composition Mechanism for Refinement-Based Methods.
Proceedings of the 22nd International Conference on Engineering of Complex Computer Systems, 2017
Extending ERS for Modelling Dynamic Workflows in Event-B.
Proceedings of the 22nd International Conference on Engineering of Complex Computer Systems, 2017
Formal Analysis of Safety and Security Requirements of Critical Systems Supported by an Extended STPA Methodology.
Proceedings of the 2017 IEEE European Symposium on Security and Privacy Workshops, 2017
2016
Editorial.
Formal Asp. Comput., 2016
Formal Modelling, Testing and Verification of HSA Memory Models using Event-B.
CoRR, 2016
Modelling Hybrid Systems in Event-B and Hybrid Event-B: A Comparison of Water Tanks.
Proceedings of the Formal Methods and Software Engineering, 2016
Validating the Requirements and Design of a Hemodialysis Machine Using iUML-B, BMotion Studio, and Co-Simulation.
Proceedings of the Abstract State Machines, Alloy, B, TLA, VDM, and Z, 2016
A Graphical Tool for Event Refinement Structures in Event-B.
Proceedings of the Abstract State Machines, Alloy, B, TLA, VDM, and Z, 2016
Modelling and Refining Hybrid Systems in Event-B and Rodin.
Proceedings of the From Action Systems to Distributed Systems - The Refinement Approach., 2016
2015
A method of refinement in UML-B.
Software and System Modeling, 2015
Core Hybrid Event-B I: Single Hybrid Event-B machines.
Sci. Comput. Program., 2015
Building traceable Event-B models from requirements.
Sci. Comput. Program., 2015
Language and tool support for event refinement structures in Event-B.
Formal Asp. Comput., 2015
Editorial.
Formal Asp. Comput., 2015
Editorial.
Formal Asp. Comput., 2015
Transforming Event-B Models to Dafny Contracts.
ECEASST, 2015
Towards Automatic Code Generation of Run-Time Power Management for Embedded Systems Using Formal Methods.
Proceedings of the IEEE 9th International Symposium on Embedded Multicore/Many-core Systems-on-Chip, 2015
From Event-B Models to Dafny Code Contracts.
Proceedings of the Fundamentals of Software Engineering - 6th International Conference, 2015
2014
Co-simulating event-B and continuous models via FMI.
Proceedings of the 2014 Summer Simulation Multiconference, 2014
A Systematic Approach to Requirements Driven Test Generation for Safety Critical Systems.
Proceedings of the Model-Based Safety and Assessment - 4th International Symposium, 2014
Applying an Integrated Modelling Process to Run-time Management of Many-Core Systems.
Proceedings of the Integrated Formal Methods - 11th International Conference, 2014
Formal Derivation of Distributed MapReduce.
Proceedings of the Abstract State Machines, Alloy, B, TLA, VDM, and Z, 2014
2013
Mastering System Analysis and Design through Abstraction and Refinement.
Proceedings of the Engineering Dependable Software Systems, 2013
Reasoned modelling critics: Turning failed proofs into modelling guidance.
Sci. Comput. Program., 2013
Editorial.
Formal Asp. Comput., 2013
Evaluation of Graphical Control Flow Management Approaches for Event-B Modelling.
ECEASST, 2013
Building Traceable Event-B Models from Requirements.
ECEASST, 2013
Modelling and Refinement in CODA
Proceedings of the Proceedings 16th International Refinement Workshop, 2013
Systematic Development of Control Designs via Formal Refinement.
Proceedings of the MODELSWARD 2013 - Proceedings of the 1st International Conference on Model-Driven Engineering and Software Development, Barcelona, Spain, 19, 2013
Problem decomposition and sub-model reconciliation of control systems in Event-B.
Proceedings of the IEEE 14th International Conference on Information Reuse & Integration, 2013
Cruise Control in Hybrid Event-B.
Proceedings of the Theoretical Aspects of Computing - ICTAC 2013, 2013
A Hybrid Event-B Study of Lane Centering.
Proceedings of the Complex Systems Design & Management, 2013
A mixed approach to rigorous development of control designs.
Proceedings of the 2013 IEEE International Symposium on Computer-Aided Control System Design, 2013
Practical Theory Extension in Event-B.
Proceedings of the Theories of Programming and Formal Methods, 2013
Tooling.
Proceedings of the Industrial Deployment of System Engineering Methods, 2013
2012
External and internal choice with event groups in Event-B.
Formal Asp. Comput., 2012
Building on the DEPLOY Legacy: Code Generation and Simulation
CoRR, 2012
A Systematic Approach to Atomicity Decomposition in Event-B.
Proceedings of the Software Engineering and Formal Methods - 10th International Conference, 2012
A Practical Approach for Closed Systems Formal Verification Using Event-B.
Proceedings of the Software Engineering and Formal Methods - 10th International Conference, 2012
Control Systems: Phenomena and Structuring Functional Requirement Documents.
Proceedings of the 17th IEEE International Conference on Engineering of Complex Computer Systems, 2012
Event-B Code Generation: Type Extension with Theories.
Proceedings of the Abstract State Machines, Alloy, B, VDM, and Z, 2012
Formal Modelling for Ada Implementations: Tasking Event-B.
Proceedings of the Reliable Software Technologies - Ada-Europe 2012, 2012
2011
Decomposition tool for event-B.
Softw., Pract. Exper., 2011
Structuring Functional Requirements of Control Systems to Facilitate Refinement-based Formalisation.
ECEASST, 2011
Specification and refinement of discrete timing properties in Event-B.
ECEASST, 2011
Composing Event-B Specifications - Case-Study Experience.
Proceedings of the Software Composition - 10th International Conference, SC 2011, Zurich, 2011
Applying Atomicity and Model Decomposition to a Space Craft System in Event-B.
Proceedings of the NASA Formal Methods, 2011
2010
Rodin: an open toolset for modelling and reasoning in Event-B.
STTT, 2010
Editorial.
Formal Asp. Comput., 2010
Rewriting and Well-Definedness within a Proof System
Proceedings of the Proceedings Workshop on Partiality and Recursion in Interactive Theorem Provers, 2010
Deriving Relationship Between Semantic Models - An Approach for cCSP
CoRR, 2010
Formalizing cCSP Synchronous Semantics in PVS
CoRR, 2010
Evaluation of a Guideline by Formal Modelling of Cruise Control System in Event-B.
Proceedings of the Second NASA Formal Methods Symposium, 2010
Rewriting and Well-Definedness within a Proof System.
Proceedings of the Partiality and Recursion in Interactive Theorem Provers, 2010
Verification of UML Models by Translation to UML-B.
Proceedings of the Formal Methods for Components and Objects - 9th International Symposium, 2010
Shared Event Composition/Decomposition in Event-B.
Proceedings of the Formal Methods for Components and Objects - 9th International Symposium, 2010
A Refinement-Based Correctness Proof of Symmetry Reduced Model Checking.
Proceedings of the Abstract State Machines, 2010
A Basis for Feature-Oriented Modelling in Event-B.
Proceedings of the Abstract State Machines, 2010
On an Extensible Rule-Based Prover for Event-B.
Proceedings of the Abstract State Machines, 2010
Reasoned Modelling Critics: Turning Failed Proofs into Modelling Guidance.
Proceedings of the Abstract State Machines, 2010
2009
Formal Development of a Total Order Broadcast for Distributed Transactions Using Event-B.
Proceedings of the Methods, 2009
Event-B Patterns for Specifying Fault-Tolerance in Multi-agent Interaction.
Proceedings of the Methods, 2009
PVS Embedding of cCSP Semantic Models and Their Relationship.
Electr. Notes Theor. Comput. Sci., 2009
Applying Event and Machine Decomposition to a Flash-Based Filestore in Event-B.
Proceedings of the Formal Methods: Foundations and Applications, 2009
Decomposition Structures for Event-B.
Proceedings of the Integrated Formal Methods, 7th International Conference, 2009
Supporting Reuse of Event-B Developments through Generic Instantiation.
Proceedings of the Formal Methods and Software Engineering, 2009
Verification of Liveness Properties in Distributed Systems.
Proceedings of the Contemporary Computing - Second International Conference, 2009
Applying Event-B Atomicity Decomposition to a Multi Media Protocol.
Proceedings of the Formal Methods for Components and Objects - 8th International Symposium, 2009
Language and Tool Support for Class and State Machine Refinement in UML-B.
Proceedings of the FM 2009: Formal Methods, 2009
09381 Extended Abstracts Collection - Refinement Based Methods for the Construction of Dependable Systems.
Proceedings of the Refinement Based Methods for the Construction of Dependable Systems, 13.09., 2009
Validating and Animating Higher-Order Recursive Functions in B.
Proceedings of the Rigorous Methods for Software Construction and Analysis, 2009
2008
ProB: an automated analysis toolset for the B method.
STTT, 2008
An incremental development of the Mondex system in Event-B.
Formal Asp. Comput., 2008
Linking Event-B and Concurrent Object-Oriented Programs.
Electr. Notes Theor. Comput. Sci., 2008
Modelling and Proof of a Tree-Structured File System in Event-B and Rodin.
Proceedings of the Formal Methods and Software Engineering, 2008
UML-B: A Plug-in for the Event-B Tool Set.
Proceedings of the Abstract State Machines, B and Z, First International Conference, 2008
A Roadmap for the Rodin Toolset.
Proceedings of the Abstract State Machines, B and Z, First International Conference, 2008
2007
Symmetry Reduced Model Checking for B.
Proceedings of the First Joint IEEE/IFIP Symposium on Theoretical Aspects of Software Engineering, 2007
Automatic Testing from Formal Specifications.
Proceedings of the Tests and Proofs, First International Conference, 2007
Symmetry Reduction for B by Permutation Flooding.
Proceedings of the B 2007: Formal Specification and Development in B, 2007
2006
UML-B: Formal modeling and design aided by UML.
ACM Trans. Softw. Eng. Methodol., 2006
Guest Editorial Editorial for the FAC Special Issue based on derivative papers from "Refine '05".
Formal Asp. Comput., 2006
Rigorous Design of Fault-Tolerant Transactions for Replicated Database Systems Using Event B.
Proceedings of the Rigorous Development of Complex Fault-Tolerant Systems [FP6 IST-511599 RODIN project], 2006
An Open Extensible Tool Environment for Event-B.
Proceedings of the Formal Methods and Software Engineering, 2006
Roadmap for enhanced languages and methods to aid verification.
Proceedings of the Generative Programming and Component Engineering, 2006
A Proposal for Records in Event-B.
Proceedings of the FM 2006: Formal Methods, 2006
2005
Precise Modelling of Compensating Business Transactions and its Application to BPEL.
J. UCS, 2005
ProTest: An Automatic Test Environment for B Specifications.
Electr. Notes Theor. Comput. Sci., 2005
Some Guidelines for Formal Development of Web-Based Applications in B-Method.
Proceedings of the ZB 2005: Formal Specification and Development in Z and B, 2005
Automatic Refinement Checking for B.
Proceedings of the Formal Methods and Software Engineering, 2005
Combining CSP and B for Specification and Property Verification.
Proceedings of the FM 2005: Formal Methods, 2005
Executable Semantics for Compensating CSP.
Proceedings of the Formal Techniques for Computer Systems and Business Processes, 2005
Comparing Two Approaches to Compensable Flow Composition.
Proceedings of the CONCUR 2005 - Concurrency Theory, 16th International Conference, 2005
Tools for System Validation with B Abstract Machines.
Proceedings of the 12th International Workshop on Abstract State Machines, 2005
2004
Performance analysis of probabilistic action systems.
Formal Asp. Comput., 2004
The Use of Formal Methods in the Analysis of Trust (Position Paper).
Proceedings of the Trust Management, Second International Conference, 2004
An Operational Semantics for StAC, a Language for Modelling Long-Running Business Transactions.
Proceedings of the Coordination Models and Languages, 6th International Conference, 2004
A Trace Semantics for Long-Running Transactions.
Proceedings of the Communicating Sequential Processes: The First 25 Years, 2004
A Trust Analysis Methodology for Pervasive Computing Systems.
Proceedings of the Trusting Agents for Trusting Electronic Societies, 2004
2003
Using B Refinement to Analyse Compensating Business Processes.
Proceedings of the ZB 2003: Formal Specification and Development in Z and B, 2003
Towards Formalizing UML State Diagrams in CSP.
Proceedings of the 1st International Conference on Software Engineering and Formal Methods (SEFM 2003), 2003
ProB: A Model Checker for B.
Proceedings of the FME 2003: Formal Methods, 2003
Using SPIN and STeP to Verify Business Processes Specifications.
Proceedings of the Perspectives of Systems Informatics, 2003
2002
Extending the concept of transaction compensation.
IBM Systems Journal, 2002
On the Use of Data Refinement in the Development of Secure Communications Systems.
Formal Asp. Comput., 2002
A System-Based Approach to the Formal Development of Embedded Controllers for a Railway.
Design Autom. for Emb. Sys., 2002
An Approach to Combining B and Alloy.
Proceedings of the ZB 2002: Formal Specification and Development in Z and B, 2002
Tool Support for Visualizing CSP in UML.
Proceedings of the Formal Methods and Software Engineering, 2002
2001
Using a Graphical Design Tool for Formal Specification.
Proceedings of the 13th Annual Workshop of the Psychology of Programming Interest Group, 2001
Transacted Memory for Smart Cards.
Proceedings of the FME 2001: Formal Methods for Increasing Software Productivity, 2001
2000
csp2B: A Practical Approach to Combining CSP and B.
Formal Asp. Comput., 2000
Performing Algorithmic Refinement before Data Refinement in B.
Proceedings of the ZB 2000: Formal Specification and Development in Z and B, First International Conference of B and Z Users, York, UK, August 29, 2000
A Generic Model for Assessing Process Quality.
Proceedings of the New Approaches in Software Measurement, 10th International Workshop, 2000
A Process Compensation Language.
Proceedings of the Integrated Formal Methods, Second International Conference, 2000
1999
Reasoning about Grover's quantum search algorithm using probabilistic wp.
ACM Trans. Program. Lang. Syst., 1999
Calculational Derivation of Pointer Algorithms from Tree Operations.
Sci. Comput. Program., 1999
The Operational Semantics of a Java Secure Processor.
Proceedings of the Formal Syntax and Semantics of Java, 1999
csp2B: A Practical Approach to Combining CSP and B.
Proceedings of the FM'99 - Formal Methods, 1999
1998
Fusion and Simultaneous Execution in the Refinement Calculus.
Acta Inf., 1998
1997
An Approach to the Design of Distributed Systems with B AMN.
Proceedings of the ZUM '97: The Z Formal Specification Notation, 1997
1996
Stepwise Refinement of Communicating Systems.
Sci. Comput. Program., 1996
Program Derivation Using the Refinement Calculator.
Proceedings of the Theorem Proving in Higher Order Logics, 9th International Conference, 1996
1995
Action Systemes, Unbounded Nondeterminism, and Infinite Traces.
Formal Asp. Comput., 1995
Exploring Summation and Product Operators in the Refinement Calculus.
Proceedings of the Mathematics of Program Construction, 1995
An Action System Approach to the Steam Boiler Problem.
Proceedings of the Formal Methods for Industrial Applications, 1995
1993
Refinement and Decomposition of Value-Passing Action Systems.
Proceedings of the CONCUR '93, 1993
1992
A CSP approach to action systems.
PhD thesis, 1992
1991
Behavioural Extension for CSP.
Proceedings of the VDM '91, 1991
1990
Service Extension at the Specification Level.
Proceedings of the Z User Workshop, 1990