Michael J. Butler

Orcid: 0000-0003-4642-5373

Affiliations:
  • University of Southampton, UK


According to our database1, Michael J. Butler authored at least 186 papers between 1990 and 2024.

Collaborative distances:
  • Dijkstra number2 of two.
  • Erdős number3 of three.

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Dataset
Other 

Links

Online presence:

On csauthors.net:

Bibliography

2024
An AIC-based approach for articulating unpredictable problems in open complex environments.
CoRR, 2024

An Event-B Formal Model for Access Control and Resource Management of Serverless Apps.
Proceedings of the Rigorous State-Based Methods - 10th International Conference, 2024

Semantics Formalisation - From Event-B Contexts to Theories.
Proceedings of the Rigorous State-Based Methods - 10th International Conference, 2024

Designing Exception Handling Using Event-B.
Proceedings of the Rigorous State-Based Methods - 10th International Conference, 2024

Event-B Development of Modelling Human Intervention Request in Self-driving Vehicle Systems.
Proceedings of the Rigorous State-Based Methods - 10th International Conference, 2024

CuneiForm Method for Assuring the Safety of ML-Based Computer Vision Development Datasets.
Proceedings of the 32nd IEEE International Requirements Engineering Conference, 2024

2023
A fairness-based refinement strategy to transform liveness properties in Event-B models.
Sci. Comput. Program., 2023

Designing Critical Systems Using Hierarchical STPA and Event-B.
Proceedings of the Rigorous State-Based Methods - 9th International Conference, 2023

Verifiably Safe and Trusted Human-AI Systems: A Socio-technical Perspective.
Proceedings of the First International Symposium on Trustworthy Autonomous Systems, 2023

Formal Language Semantics for Triggered Enable Statecharts with a Run-to-Completion Scheduling.
Proceedings of the Theoretical Aspects of Computing - ICTAC 2023, 2023

AIC Approach for Intelligent Systems Requirements Elicitation.
Proceedings of the 7th International Conference on System Reliability and Safety, 2023

A Rigorous Iterative Analysis Approach for Capturing the Safety Requirements of Self-Driving Vehicle Systems.
Proceedings of the 47th IEEE Annual Computers, Software, and Applications Conference, 2023

2022
Formal verification and validation of run-to-completion style state charts using Event-B.
Innov. Syst. Softw. Eng., 2022

Developing the UML-B Modelling Tools.
Proceedings of the Software Engineering and Formal Methods. SEFM 2022 Collocated Workshops, 2022

Building an Extensible Textual Framework for the Rodin Platform.
Proceedings of the Software Engineering and Formal Methods. SEFM 2022 Collocated Workshops, 2022

A lightweight approach to the concurrent use and integration of SysML and formal methods in systems design.
Proceedings of the 25th International Conference on Model Driven Engineering Languages and Systems: Companion Proceedings, 2022

Generating SPARK from Event-B, Providing Fundamental Safety and Security.
Proceedings of the Advances in Model and Data Engineering in the Digitalization Era, 2022

High-Level Rigorous Template for Analysing Safety Properties of Self-driving Vehicle Systems.
Proceedings of the 46th IEEE Annual Computers, Software, and Applications Conferenc, 2022

2021
Domain-specific scenarios for refinement-based methods.
J. Syst. Archit., 2021

Reasoning About Real-Time Systems in Event-B Models with Fairness Assumptions.
Proceedings of the International Symposium on Theoretical Aspects of Software Engineering, 2021

Refinable Record Structures in Formal Methods.
Proceedings of the Advances in Model and Data Engineering in the Digitalization Era, 2021

The CamilleX Framework for the Rodin Platform.
Proceedings of the Rigorous State-Based Methods - 8th International Conference, 2021

Extensible Record Structures in Event-B.
Proceedings of the Rigorous State-Based Methods - 8th International Conference, 2021

Verifying System-Level Security of a Smart Ballot Box.
Proceedings of the Rigorous State-Based Methods - 8th International Conference, 2021

2020
Introduction to special section on the ABZ 2018 case study: Hybrid ERTMS/ETCS Level 3.
Int. J. Softw. Tools Technol. Transf., 2020

Formalizing hierarchical scheduling for refinement of real-time systems.
Sci. Comput. Program., 2020

Abstract State Machines, Alloy, B, TLA, VDM and Z (ABZ 2018).
Sci. Comput. Program., 2020

Trace semantics and refinement patterns for real-time properties in event-B models.
Sci. Comput. Program., 2020

Verifying Cross-Layer Interactions Through Formal Model-Based Assertion Generation.
IEEE Embed. Syst. Lett., 2020

Real-Time Trigger-Response Properties for Event-B Applied to the Pacemaker.
Proceedings of the International Symposium on Theoretical Aspects of Software Engineering, 2020

The First Twenty-Five Years of Industrial Use of the B-Method.
Proceedings of the Formal Methods for Industrial Critical Systems, 2020

Formal Verification of Run-to-Completion Style Statecharts Using Event-B.
Proceedings of the Software Architecture - 14th European Conference, 2020

Refinement and Verification of Responsive Control Systems.
Proceedings of the Rigorous State-Based Methods - 7th International Conference, 2020

2019
A methodology for assuring the safety and security of critical infrastructure based on STPA and Event-B.
Int. J. Crit. Comput. Based Syst., 2019

Towards Refinement Semantics of Real-Time Trigger-Response Properties in Event-B.
Proceedings of the 2019 International Symposium on Theoretical Aspects of Software Engineering, 2019

Domain-Specific Scenarios for Refinement-Based Methods.
Proceedings of the New Trends in Model and Data Engineering, 2019

Behaviour-Driven Formal Model Development of the ETCS Hybrid Level 3.
Proceedings of the 24th International Conference on Engineering of Complex Computer Systems, 2019

SEB-CG: Code Generation Tool with Algorithmic Refinement Support for Event-B.
Proceedings of the Formal Methods. FM 2019 International Workshops, 2019

Making (Implicit) Security Requirements Explicit for Cyber-Physical Systems: A Maritime Use Case Security Analysis.
Proceedings of the Database and Expert Systems Applications, 2019

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.
J. Syst. Archit., 2018

DeepSaucer: Unified Environment for Verifying Deep Neural Networks.
CoRR, 2018

Semantics of Real-Time Trigger-Response Properties in Event-B.
Proceedings of the 2018 International Symposium on Theoretical Aspects of Software Engineering, 2018

Developing A New Language to Construct Algebraic Hierarchies for Event-B.
Proceedings of the Dependable Software Engineering. Theories, Tools, and Applications, 2018

Behaviour-Driven Formal Model Development.
Proceedings of the Formal Methods and Software Engineering, 2018

Reusing Formal Models via Lifting.
Proceedings of the 23rd International Conference on Engineering of Complex Computer Systems, 2018

Refinement of Statecharts with Run-to-Completion Semantics.
Proceedings of the Formal Techniques for Safety-Critical Systems, 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 Aspects 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.
Softw. Syst. Model., 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 Aspects Comput., 2015

Editorial.
Formal Aspects Comput., 2015

Editorial.
Formal Aspects Comput., 2015

Transforming Event-B Models to Dafny Contracts.
Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 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

Co-simulation Environment for Rodin: Landing Gear Case Study.
Proceedings of the ABZ 2014: The Landing Gear Case Study, 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 Aspects Comput., 2013

Evaluation of Graphical Control Flow Management Approaches for Event-B Modelling.
Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 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 Aspects 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. Exp., 2011

Structuring Functional Requirements of Control Systems to Facilitate Refinement-based Formalisation.
Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 2011

Specification and refinement of discrete timing properties in Event-B.
Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 2011

Composing Event-B Specifications - Case-Study Experience.
Proceedings of the Software Composition - 10th International Conference, 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.
Int. J. Softw. Tools Technol. Transf., 2010

Editorial.
Formal Aspects 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

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

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.
Int. J. Softw. Tools Technol. Transf., 2008

An incremental development of the Mondex system in Event-B.
Formal Aspects Comput., 2008

PVS Embedding of cCSP Semantic Models and Their Relationship.
Proceedings of the Eighth International Workshop on Automated Verification of Critical Systems, 2008

Linking Event-B and Concurrent Object-Oriented Programs.
Proceedings of the 13th BAC-FACS Refinement Workshop, 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 - 1st 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 Aspects 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. Univers. 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 Aspects Comput., 2004

ProTest: An Automatic Test Environment for B Specifications.
Proceedings of the Workshop on Model Based Testing, 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 Syst. J., 2002

On the Use of Data Refinement in the Development of Secure Communications Systems.
Formal Aspects Comput., 2002

A System-Based Approach to the Formal Development of Embedded Controllers for a Railway.
Des. Autom. Embed. Syst., 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 Aspects 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 <i>wp</i>.
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

1998
Fusion and Simultaneous Execution in the Refinement Calculus.
Acta Informatica, 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 Aspects 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


  Loading...