Dean of the Faculty of Engineering and Physical Sciences
Michael Butler is Dean of the Faculty of Engineering and Physical Sciences and a Professor of Computer Science. His research is in the area of mathematical methods for design and verification of safe and secure software-based systems.
Education:
B.A.(Hons) Computer Science, Trinity College Dublin (1988);
M.Sc. Computation, University of Oxford (1989);
D.Phil. Computation, University of Oxford (1992).
My main research area is formal methods for software engineering. These are mathematical modeling and analysis methods used to increase the trustworthiness of software based systems. They are typically used for high integrity systems where software-induced failures would lead to loss of life or significant loss of business or reputation. I specialise in model-based formal methods, in particular a formal method called Event-B. My research work encompasses applications, tools and methodology for formal methods. I have made key theoretical and methodological contributions to the Event-B formal method that enable it to scale to large complex systems. These contributions enable modular analysis in terms of how systems models are structured and analysed as well as methods for development of domain-specific mathematical theories that are reusable across multiple projects.
Research Projects
HD-Sec: Holistic Design of Secure Systems on Capability Hardware
HICLASS: Enabling Development of Complex and Secure Aerospace Systems
UKRI Trustworthy Autonomous Systems Hub
Professional Activities:
Member IFIP WG 2.3 Programming Methodology
Editorial Board of Formal Aspects of Computing
Editorial Board of Intl. J. of Critical Computer-Based Systems
Editorial Board of Software Tools for Technology Transfer
Silva, Renato and Butler, Michael (2009) Supporting reuse of Event-B developments through generic instantiation. Formal Methods and Software Engineering, 11th International Conference on Formal Engineering Methods, ICFEM 2009, Rio de Janeiro, Brazil. 09 - 12 Dec 2009. 19 pp . (doi:10.1007/978-3-642-10373-5_24).
Sorge, Jennifer, Poppleton, Michael and Butler, Michael (2009) A Basis for feature-oriented modelling in Event-B s.n.
Silva, Renato and Butler, Michael (2009) Supporting reuse mechanisms for developments in event-b: composition Southampton, UK. University of Southampton 15pp.
Pascal, Carine and Silva, Renato (2009) Event-B model decomposition. DEPLOY Plenary Technical Workshop 2009. 20 - 22 Oct 2009. 6 pp .
Silva, Renato, Pascal, Carine, Hoang, T.S. and Butler, Michael (2009) Decomposition tool for Event-B Southampton, UK. University of Southampton 4pp.
Maamria, Issam, Butler, Michael, Edmunds, Andrew and Rezazadeh, Abdolbaghi (2010) On an extensible rule-based prover for event-B. In Proceedings of ABZ 2010. Springer. 3 pp .
Butler, M. J. and Hartel, P. H. (1999) Reasoning about Grover's Quantum Search Algorithm using Probabilistic wp. ACM Transactions on Programming Languages and Systems, 21 (3), 417-430.
Butler, M. J. (1999) Calculational Derivation of Pointer Algorithms from Tree Operations. Science of Computer Programming, 33 (3), 221-260.
Butler, M. J. (1999) csp2B: A Practical Approach to Combining CSP and B. Wing, J. M., Woodcock, J. and Davies, J. (eds.) Proc. FM'99: World Congress on Formal Methods. pp. 490-508 .
Butler, M. J. (1999) Distributed Electronic Mail System. Sekerinski, E. and Sere, K. (eds.) Program Development by Refinement - Case Studies Using the B Method, Springer FACIT Series. pp. 301-322 .
Butler, M. J. and Waldén, M. (1999) Parallel Programming with the B Method. Sekerinski, E. and Sere, K. (eds.) Program Development by Refinement - Case Studies Using the B Method, Springer FACIT Series. pp. 183-195 .
Hartel, P. H., Butler, M. J. and Levy, M. (1999) The Operational Semantics of a Java Secure Processor. In, Alves-Foss, J. (ed.) Formal Syntax and Semantics of Java, LNCS 1523. Formal Syntax and Semantics of Java, LNCS 1523 (01/01/99) Springer Verlag, pp. 313-52.
Hartel, P., Butler, M., Currie, A., Henderson, P., Leuschel, M., Martin, A., Smith, A., Ultes-Nitsche, U. and Walters, R.J. (1999) Questions and Answers About Ten Formal Methods. Gnesi, S. and latella, D. (eds.) Proc. 4th Int. Workshop on Formal Methods for Industrial Critical Systems. pp. 179-203 .
Back, R. J. R. and Butler, M. J. (1998) Fusion and Simultaneous Execution in the Refinement Calculus. Acta Informatica, 35 (11), 921-949.
Butler, M. J. (1998) Event Ordering in Action Systems. Grundy, J., Schwenke, M. and Vickers, T. (eds.) Proc. Int. Refinement Workshop / Formal Methods Pacific'98, Springer Series in Discrete Mathematics and Theoretical Computer Science. pp. 61-80 .
Butler, M. J. (1998) Using Refinement to Analyse the Safety of an Authentication Protocol s.n.
Butler, M. J. (1997) An Approach to the Design of Distributed Systems with B AMN. Bowen, J., Hinchey, M. and Till, D. (eds.) Proc. 10th Int. Conf. of Z Users: The Z Formal Specification Notation (ZUM), LNCS 1212. pp. 223-241 .
Butler, M. J. (1997) Review of Abrial, J.-R. The B-Book. The Computer Journal, 40 (1), 59-61.
Butler, M. J., Grundy, J., Långbacka, T., Ruksenas, R. and Wright, J. von (1997) The Refinement Calculator: Proof Support for Program Refinement. Groves, L. and Reeves, S. (eds.) Proc. Conf. Formal Methods Pacific'97, Springer Series in Discrete Mathematics and Theoretical Computer Science. pp. 40-61 .
Butler, M. J. (1997) Action System Analysis of an Authentication Protocol (extended abstract). Groves, L. and Reeves, S. (eds.) Proc. Conf. Formal Methods Pacific'97, Springer Series in Discrete Mathematics and Theoretical Computer Science. pp. 287-288 .
Butler, M. J. (1996) Stepwise Refinement of Communicating Systems. Science of Computer Programming, 27 (2), 139-173.
Butler, M. J. (1996) Calculational Derivation of Algorithms on Tree-based Pointer Structures. Jifeng, He, Cooke, J. and Wallace, P. (eds.) BCS-FACS Refinement Workshop.
Butler, M. J. (1996) An Approach to the Design of Distributed Systems with B AMN (extended version) s.n.
Butler, M. J. and Långbacka, T. (1996) Program Derivation using the Refinement Calculator. Wright, J. von, Grundy, J. and Harrison, J. (eds.) Proc. 9th Int. Conf. on Theorem Proving in Higher Order Logics (TPHOLs'96), LNCS 1125. pp. 93-108 .
Butler, M. J., Sekerinski, E. and Sere, K. (1996) An Action System Approach to the Steam Boiler Problem. Abrial, J.-R., Börger, E. and Langmaack, H. (eds.) Formal Methods for Industrial Applications -- Specifying and Programming the Steam Boiler Control, LNCS 1165. pp. 129-148 .
Butler, M. J. and Waldén, M. (1996) Distributed System Development in B. Habrias, H. (ed.) Proc. First B Conf.. pp. 155-168 .
Butler, M.J. and Morgan, C.C. (1995) Action Systems, Unbounded Nondeterminism, and Infinite Traces. Formal Aspects of Computing, 7, 37-53.
Back, R.J.R. and Butler, M.J. (1995) Exploring Summation and Product Operators in the Refinement Calculus. Möller, B. (ed.) Mathematics of Program Construction.
Butler, M.J. (1993) Refinement and decomposition of value-passing action systems in the refinement calculus. In, Best, E. and Best, E. (eds.) CONCUR'93. (Lecture Notes in Computer Science, 715) 4th Intrenational Conference on Concurrency Theory (22/08/93 - 26/08/93) Berlin, Heidelberg. Springer. (doi:10.1007/3-540-57208-2_16).
Butler, M.J. (1991) Behavioural Extension for CSP Processes. Prehn, S. and Toetenel, W.J. (eds.) VDM '91.
Butler, M.J. (1990) Service Extension at the Specification Level. Nicholls, J.E. (ed.) Z User Meeting.
Butler, M.J., Hedman, E., Nilson, P., Ruksenas, R., Waldén, M. and Zhao, Y. (1994) Specification of a Program Derivation Editor (Reports in Mathematics and Computer Science, A94-15) s.n.
Butler, M.J. and Back, R.J.R. (1994) Applications of Summation and Product Operators in the Refinement Calculus. 6th Nordic Workshop on Programming Theory.
Butler, M.J. (1989) Formal Techniques Applied to the X.400 Reliable Transfer Service. University of Oxford, Masters Thesis.
Butler, M.J. (1992) A CSP Approach to Action Systems. University of Oxford, Computing Laboratory, Doctoral Thesis.
Butler, M.J. (1993) Feature Interaction Analysis Using Z s.n.
Butler, M. J. and Meagher, M. M. R. (2000) Performing Algorithmic Refinement before Data Refinement in B. Proc. ZB2000: Formal Specification and Development in Z and B. pp. 324-343 .
Hallerstede, S. and Butler, M. J. (1999) Refinement of Dynamic Systems University of Southampton
Butler, M. J. (2000) csp2B: A Practical Approach to Combining CSP and B. Formal Aspects of Computing, 12, 182-196.
Satpathy, Manoranjan, Harrison, Rachel, Snook, Colin and Butler, Michael (2001) A Generic Model for Assessing Process Quality. Dumke, None and Abran, None (eds.) International Workshop on Software Measurement (IWSM2000).
Butler, Michael and Ferreira, Carla (2000) A Process Compensation Language. Grieskamp, W., Santen, T. and Stoddart, B. (eds.) Integrated Formal Methods IFM2000. p. 61 .
Butler, Michael, Hartel, Pieter, Jong, Eduard de and Longley, Mark (1997) Applying Formal Methods to the Design of Smart Card Software s.n.
Butler, Michael and Airchinnigh, Micheal Mac an (1993) Service Specification Using Z s.n.
Butler, Michael and McDonnell, Eoin (1993) Experiment D: Application of Z to IN-Services Test Case s.n.
Butler, Michael, Hartel, Pieter, Jong, Eduard de and Longley, Mark (2001) Transacted Memory for Smart Cards. Oliveira, J. N. and Zave, P. (eds.) FME 2001, Formal Methods for Increasing Software Productivity. pp. 478-99 .
Snook, Colin and Butler, Michael (2000) Verifying Dynamic Properties of UML Models by Translation to the B Language and Toolkit. UML 2000 Workshop, Dynamic Behaviour in UML Models: Semantic Questions.
Snook, C. and Butler, M. J. (2001) Using a Graphical Design Tool for Formal Specification. Proceedings 13th Annual Workshop of the Psychology of Programming Interest Group.
Mikhailov, Leonid and Butler, Michael (2001) Combining B and Alloy. Formal Methods for Industrial Critical Systems.
Satpathy, Manoranjan, Harrison, Rachel, Snook, Colin and Butler, Michael (2001) A Comparative Study of Formal and Informal Specifications through an Industrial Case Study. IEEE/ IFIP Workshop on Formal Specification of Computer Based Systems (FSCBS'01).
DeRoure, David, Moreau, Luc, Butler, Michael, Chown, Tim and Hartel, Pieter (2000) Study of Security in Multi-Agent Architectures Department of Electronics and Computer Science, University of Southampton
Leuschel, Michael, Adhianto, Laksono, Butler, Michael, Ferreira, Carla and Mikhailov, Leonid (2001) Animation and Model Checking of CSP and B using Prolog Technology. Leuschel, Michael, Podelski, Andreas, Ramakrishnan, C.R. and Ultes-Nitsche, Ulrich (eds.) Proceedings of the ACM Sigplan Workshop on Verification and Computational Logic VCL'2001. pp. 97-109 .
Mikhailov, Leonid and Butler, Michael (2002) An Approach to Combining B and Alloy. ZB'2002.
Butler, Michael (2002) A System-based Approach to the Formal Development of Embedded Controllers for a Railway. Design Automation for Embedded Systems, 6, 355-366.
Butler, Michael and Falampin, Jerome (2002) An Approach to Modelling and Refining Timing Properties in B. Refinement of Critical Systems (RCS).
Mikhailova, Anna, Doche, Marielle and Butler, Michael (2002) Contracts for Scenario-Based Testing of Object-Oriented Programs s.n.
Ng, Muan Yong and Butler, Michael (2002) Tool Support for Visualizing CSP in UML. George, Chris and Miao, HuaiKou (eds.) International Conference on Formal Engineering Methods(ICFEM), Shanghai, China. 20 - 24 Oct 2002. pp. 287-298 .
Butler, Michael, Leuschel, Michael, Lo Presti, Stephane, Allsopp, David, Beautement, Patrick, Booth, Chris, Cusack, Mark and Kirton, Mike (2003) Towards a Trust Analysis Framework for Pervasive Computing Scenarios.
Butler, Michael, Ferreira, Carla, Henderson, Peter, Chessell, Mandy, Griffin, Catherine and Vines, David (2002) Extending the Concept of Transaction Compensation. IBM Systems Journal, 47, 743-758.
Augusto, Juan Carlos, Leuschel, Michael, Butler, Michael and Ferreira, Carla (2003) Using the Extensible Model Checker XTL to Verify StAC Business Specifications. Leuschel, Michael, Gruner, Stefan and Lo Presti, Stephane (eds.) 3rd Workshop on Automated Verification of Critical Systems (AVoCS 2003), Southampton. 01 - 02 Apr 2003. pp. 253-266 .
Butler, M. J. (2002) On the Use of Data Refinement in the Development of Secure Communications Systems. Formal Aspects of Computing, 14 (1), 2-34.
Augusto, Juan, Butler, Michael, Ferreira, Carla and Craig, Stephen (2003) Using SPIN and STeP to Verify StAC Specifications. 5th International A.P.Ershov Conference on Perspectives of System Informatics, Novosibirsk, Russia.
Ng, Muan Yong and Butler, Michael (2003) Towards formalizing UML State Diagrams in CSP. Cerone, Antonio and Lindsay, Peter (eds.) 1st IEEE International Conference on Software Engineering and Formal Methods, Brisbane, Australia. 24 - 25 Sep 2003. pp. 138-147 .
Leuschel, Michael and Butler, Michael (2003) ProB: A Model Checker for B. Keijiro, Araki, Gnesi, Stefania and Dino, Mandrio (eds.) Formal Methods Europe 2003, Pisa, Italy. pp. 855-874 .
Butler, Michael and Ferreira, Carla (2003) Using B Refinement to Analyse Compensating Business Processes. ZB 2003: Third International Conference of B and Z Users, Turku.
Rezazadeh, Abdolbaghi and Butler, Michael (2003) Event-Based Modelling and Refinement of Distributed Monitoring and Control Systems. Refinement of Critical Systems (RCS'03).
Butler, Michael, Leuschel, Michael, Lo Presti, Stephane and Turner, Phillip (2004) The Use of Formal Methods in the Analysis of Trust (Position Paper). Jensen, Christian, Poslad, Stefan and Dimitrakos, Theo (eds.) Second International Conference on Trust Management (iTrust 2004), Oxford, United Kingdom. 01 Mar - 28 Apr 2004. pp. 333-339 .
Hallerstede, Stefan and Butler, Michael (2004) Performance Analysis of Probabilistic Action Systems. Formal Aspects of Computing, 16 (4), 313-331.
Butler, Michael and Ferreira, Carla (2004) An Operational Semantics for StAC, a Language for Modelling Long-running Business Transactions. De Nicola, Rocco, Ferrari, Gianluigi and Meredith, Greg (eds.) Coordination 2004, Pisa.
Snook, Colin, Butler, Michael and Oliver, Ian (2004) The UML-B Profile for formal systems modelling in UML. In, Mermet, J. (ed.) UML-B Specification for Proven Embedded Systems Design. Springer.
Butler, Michael, Ferreira, Carla and Ng, Muan Yong (2005) Precise Modelling of Compensating Business Transactions and its Application to BPEL. Journal of Universal Computer Science, 11 (5), 712-743.
Butler, Michael, Hoare, C.A.R. and Ferreira, Carla (2005) A trace semantics for long-running transactions. Abdallah, A.E., Jones, C.B. and Sanders, J.W. (eds.) 25 Years of CSP, London. pp. 133-150 .
Snook, Colin and Butler, Michael (2006) UML-B: Formal modelling and design aided by UML. ACM Transactions on Software Engineering and Methodology, 15 (1), 92-122.
Lo Presti, Stephane, Butler, Michael, Leuschel, Michael, Snook, Colin and Turner, Phillip (2004) Formal Modelling and Verification of Trust in a Pervasive Application s.n.
Snook, Colin, Butler, Michael, Edmunds, Andy and Johnson, Ian (2004) Rigorous development of reusable, domain-specific components, for complex applications. Jurgens, Jan and France, Robert (eds.) 3rd International Workshop on Critical Systems Development with UML, Lisbon. pp. 115-129 .
Butler, Michael and Leuschel, Michael (2005) Combining CSP and B for Specification and Property Verification. Fitzgerald, John, Hayes, Ian and Tarlecki, Andrzej (eds.) Formal Methods 2005, Newcastle upon Tyne. 17 - 21 Jul 2005. pp. 221-236 .
Rezazadeh, Abdolbaghi and Butler, Michael (2005) Some Guidelines for Formal Development of Web-based Applications in B-Method. 4th International Conference of B and Z Users (ZB 2005), 13-15 April 2005.
Satpathy, Manoranjan, Leuschel, Michael and Butler, Michael , Gurevich, Yuri, Petrenko, Alexander K. and Kossatchev, Alexander (eds.) (2005) ProTest: An Automatic Test Environment for B Specifications. Electronic Notes in Theoretical Computer Science, 111, 113-136. (doi:10.1016/j.entcs.2004.12.009).
Butler, Michael, Leuschel, Michael and Snook, Colin (2005) Tools for system validation with B abstract machines. ASM 2005: 12th International Workshop on Abstract State Machines, Paris.
Snook, Colin and Butler, Michael (2004) U2B - A tool for translating UML-B models into B. In, Mermet, J. (ed.) UML-B Specification for Proven Embedded Systems Design. Springer.
Lo Presti, S, Butler, M, Leuschel, M and Booth, C (2005) A Trust Analysis Methodology for Pervasive Computing Systems. In, Falcone, R, Barber, S, Sabater, J and Singh, M (eds.) Trusting Agents for trusting Electronic Societies, LNCS Volume 3577. Springer. (doi:10.1007/11532095).
Butler, Michael and Ripon, Shamim (2005) Executable Semantics for Compensating CSP. Bravetti, Mario, Kloul, Leïla and Zavattaro, Gianluigi (eds.) 2nd International Workshop on Web Services and Formal Methods, Versailles. 243- 256 . (doi:10.1007/11549970_18).
Lo Presti, Stephane and Butler, Michael (2005) Literature Survey on Trust s.n.
Bruni, Roberto, Butler, Michael, Ferreira, Carla, Hoare, Tony, Melgratti, Hernan and Montanari, Ugo (2005) Comparing two approaches to compensable flow composition. CONCUR 2005, San Francisco. 22 - 25 Aug 2005.
Yadav, Divakar and Butler, Michael (2005) Application of Event B to Global Causal Ordering for Fault Tolerant Transactions. Workshop on Rigorous Engineering of Fault Tolerant Systems (REFT2005), Newcastle upon Tyne. 17 - 21 Jul 2005. pp. 93-102 .
Butler, Michael, Jones, Cliff, Romanovsky, Alexander and Troubitsyna, Elena (2005) Proceedings of the Workshop on Rigorous Engineering of Fault-Tolerant Systems (REFT 2005). (Technical Report Series, CS-TR-), vol. CS-TR-, University of Newcastle upon Tyne, School of Computing Science
Leuschel, Michael and Butler, Michael (2005) Automatic Refinement Checking for B. ICFEM'05.
Evans, Neil and Butler, Michael (2006) A Proposal for Records in Event-B. Nipkow, Tobias, Misra, Jayadev and Sekerinski, Emil (eds.) Formal Methods 2006, McMaster, Canada. pp. 221-235 .
Yadav, Divakar and Butler, Michael (2006) Rigorous Design of Fault-Tolerant Transactions for Replicated Database Systems using Event B. In, Rigorous Development of Complex Fault-Tolerant Systems. Lecture Notes in Computer Science, Springer , 2006, pp. 343-363.
Ripon, Shamim and Butler, Michael (2006) Relating Semantic Models of Compensating CSP s.n.
Lo Presti, Stéphane, Butler, Michael, Leuschel, Michael and Booth, Chris (2006) Holistic Trust Design of E-Services. In, Song, Ronggong (ed.) Trust in E-services: Technologies, Practices and Challenges.
Abrial, Jean-Raymond, Butler, Michael, Hallerstede, Stefan and Voisin, Laurent (2006) An open extensible tool environment for Event-B. Liu, Zhiming and He, Jifeng (eds.) ICFEM 2006, Macau.
Evans, Neil and Butler, Michael (2006) Incremental Construction of Large Specifications: Case Study and Techniques s.n.
Turner, Edd and Butler, Michael (2006) Symmetry Reduction in the ProB Model Checker. FM2006 Doctoral Symposium, McMaster University, Canada. 20 - 26 Aug 2006.
Ball, Elisabeth and Butler, Michael (2006) Using Decomposition to Model Multi-agent Interaction Protocols in Event-B. FM'06 Doctoral Symposium, McMaster University, Hamilton, Canada.
Leavens, Gary T., Abrial, Jean-Raymond, Batory, Don, Butler, Michael, Coglio, Alessandro, Fisler, Kathi, Hehner, Eric, Jones, Cliff B., Miller, Dale, Peyton-Jones, Simon, Sitaraman, Murali, Smith, Douglas R. and Stump, Aaron (2006) Roadmap for Enhanced Languages and Methods to Aid Verification. Generative Programming and Component Engineering, 5th International, Portland, Oregon. 21 - 25 Oct 2006.
Leuschel, Michael and Butler, Michael (2008) ProB: an automated analysis toolset for the B method. International Journal on Software Tools for Technology Transfer, 10 (2), 185-203. (doi:10.1007/s10009-007-0063-9).
Leuschel, Michael, Butler, Michael, Spermann, Corinna and Turner, Edd (2006) Symmetry Reduction for B by Permutation Flooding. B2007, Besancon, France.
Butler, Michael and Yadav, Divakar (2008) An incremental development of the Mondex system in Event-B. Formal Aspects of Computing, 20 (1), 61-77. (doi:10.1007/s00165-007-0061-4).
Butler, Michael, Jones, Cliff B., Romanovsky, Alexander and Troubitsyna, Elena (2006) Rigorous Development of Complex Fault-Tolerant Systems (Lecture Notes in Computer Science, 4157), vol. 4157, Springer
Yadav, Divakar and Butler, Michael (2007) Formal Specifications and Verification of Message Ordering Properties in a Broadcasting System using Event B s.n.
Turner, Edd, Leuschel, Michael, Spermann, Corinna and Butler, Michael (2007) Symmetry Reduced Model Checking for B. First Joint IEEE/IFIP Symposium on Theoretical Aspects of Software Engineering (TASE '07), ECNU, Shanghai, China. 05 - 07 Jun 2007. pp. 25-34 .
Ball, Elisabeth and Butler, Michael (2007) Event-B Patterns for Specifying Fault-Tolerance in Multi-Agent Interaction. Methods, Models and Tools for Fault Tolerance, Oxford, United Kingdom.
Yadav, Divakar and Butler, Michael (2007) Formal Development of Fault Tolerant Transactions for a replicated Database using Ordered Broadcasts. Methods, Models and Tools for Fault Tolerance (MeMoT 2007), Oxford. pp. 33-42 .
Leuschel, Michael, Butler, Michael, Spermann, Corinna and Turner, Edd (2007) Symmetry Reduction for B by Permutation Flooding. Julliand, Jacques and Kouchnarenko, Olga (eds.) 7th International B Conference, Besancon, France. 17 - 19 Jan 2007.
Leuschel, Michael, Cansell, Dominique and Butler, Michael (2007) Validating and Animating Higher-Order Recursive Functions in B. Abrial,, Jean-Raymond and Glässer, Uwe (eds.) Festschrift for Egon Börger.
Satpathy, Manoranjan, Butler, Michael, Leuschel, Michael and Ramesh, S (2007) Automatic Testing from Formal Specifications. International Conference on Tests And Proofs (TAP), ETH Zurich, Switzerland. 12 - 13 Feb 2007.
Butler, Michael, Jones, Cliff, Romanovsky, Alexander and Troubitsyna, Elena (2007) Proceedings of the Workshop on Methods, Models and Tools for Fault Tolerance (MeMToFT 2007).
Snook, Colin and Butler, Michael (2008) UML-B and Event-B: an integration of languages and tools. The IASTED International Conference on Software Engineering - SE2008, Innsbruck, Austria. 12 - 14 Feb 2008.
Butler, Michael and Hallerstede, Stefan (2007) The Rodin Formal Modelling Tool. In BCS-FACS Christmas 2007 Meeting. BCS.. (In Press)
Rezazadeh, Abdolbaghi, Evans, Neil and Butler, Michael (2007) Redevelopment of an industrial case study using Event-B and Rodin. BCS-FACS Christmas 2007 Meeting - Formal Methods In Industry, , London, United Kingdom.
Butler, Michael (2006) On the Verified-by-Construction Approach. FACS FACTS.
Edmunds, Andrew and Butler, Michael (2008) Linking Event-B and Concurrent Object-Oriented Programs. Refine 2008 - International Refinement Workshop, Turku, Finland. (doi:10.1016/j.entcs.2008.06.008).
Damchoom, Kriangsak, Butler, Michael and Abrial, Jean-Raymond (2008) Modelling and proof of a Tree-structured File System in Event-B and Rodin. ICFEM 2008. pp. 25-44 . (doi:10.1007/978-3-540-88194-0_5).
Boerger, Egon, Butler, Michael, Bowen, Jonathan and Boca, Paul (2008) ABZ2008 Conference - Short Papers s.n. (In Press)
Börger, Egon, Butler, Michael, Bowen, Jonathan P. and Boca, Paul (2008) Abstract State Machines, B and Z - First International Conference ABZ 2008 (LNCS, 5238), vol. 5238, Springer
Abrial, Jean-Raymond, Butler, Michael, Hallerstede, Stefan and Voisin, Laurent (2008) A Roadmap for the Rodin Toolset. Abstract State Machines, B and Z, First International Conference ABZ 2008. p. 347 .
Snook, Colin and Butler, Michael (2008) UML-B: A plug-in for the Event-B tool set. Abstract State Machines, B and Z, First International Conference ABZ 2008. p. 347 .
Butler, Michael (2009) Incremental Design of Distributed Systems with Event-B. In, Broy, Manfred, Sitou, Wassiou and Hoare, Tony (eds.) Engineering Methods and Tools for Software Safety and Security - Marktoberdorf Summer School 2008. IOS Press, pp. 131-160.
Butler, Michael (2009) Decomposition Structures for Event-B. Integrated Formal Methods iFM2009, Springer, LNCS 5423.
Said, Mar Yah, Butler, Michael and Snook, Colin (2009) Class and state machine refinement in UML-B. Integration of Model-based Formal Methods and Tools (workshop at iFM 2009).
Ball, Elisabeth and Butler, Michael (2009) Event-B Patterns for Specifying Fault-Tolerance in Multi-Agent Interaction. In, Butler, M, Jones, C, Romanovsky, A and Troubitsyna, E (eds.) Methods, Models and Tools for Fault Tolerance. (Lecture Notes in Computer Science,, 5454) Springer. (doi:10.1007/978-3-642-00867-2_6).
Yadav, Divakar and Butler, Michael (2009) Formal Development of a Total Order Broadcast for Distributed Transactions using Event-B. In, Methods, Models and Tools for Fault Tolerance LNCS 5454. Springer.
Butler, Michael, Jones, Cliff B, Romanovsky, Alexander and Troubitsyna, Elena (2009) Methods, Models and Tools for Fault Tolerance (LNCS, 5454), vol. 5454, Springer
Yadav, Divakar and Butler, Michael (2009) Verification of Liveness Properties in Distributed Systems. Second International Conference, IC3 2009, Noida, India. 16 - 18 Aug 2009.
Savicks, Vitaly, Snook, Colin and Butler, Michael (2009) Animation of UML-B State-machines s.n. (Submitted)
Said, Mar Yah, Butler, Michael and Snook, Colin (2009) Language and tool support for class and state machine refinement in UML-B. Cavalcanti, A. and Dams, D. (eds.) In FM 2009: Formal Methods. Springer. pp. 579-595 . (doi:10.1007/978-3-642-05089-3_37).
Maamria, Issam, Butler, Michael, Edmunds, Andrew and Rezazadeh, Abdolbaghi (2009) On an Extensible Rule-based Prover for Event-B s.n. (In Press)
Damchoom, Kriangsak and Butler, Michael (2009) Applying Event and Machine Decomposition to a Flash-Based Filestore in Event-B. SBMF 2009, Gramado, Brazil. 18 - 20 Aug 2009. pp. 134-152 . (doi:10.1007/978-3-642-10452-7).
Abrial, Jean-Raymond, Butler, Michael, Joshi, Rajev, Troubitsyna, Elena and Woodcock, Jim C. P. (2010) 09381 Extended Abstracts Collection — Refinement Based Methods for the Construction of Dependable Systems (Dagstuhl Seminar Proceedings, 9381, 9381), vol. 9381, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Germany
Ripon, Shamim and Butler, Michael (2009) PVS Embedding of cCSP Semantic Models and their Relationship. Electr. Notes Theor. Comput. Sci., 250 (2), 103-118. (doi:10.1016/j.entcs.2009.08.020).
Ireland, Andrew, Grov, Gudmund and Butler, Michael (2010) Reasoned Modelling Critics: Turning Failed Proofs into Modelling Guidance. ABZ 2010, Orford, Canada.
Turner, Edd, Butler, Michael and Leuschel, Michael (2010) A Refinement-Based Correctness Proof of Symmetry Reduced Model Checking. ABZ 2010, Orford, Canada. (In Press)
Sorge, Jennifer, Poppleton, Mike and Butler, Michael (2010) A Basis for Feature-Oriented Modelling in Event-B. ABZ2010, Orford, Canada. 23 - 25 Feb 2010.
Silva, Renato, Pascal, Carine, Hoang, T. Son and Butler, Michael (2010) Decomposition Tool for Event-B. Workshop on Tool Building in Formal Methods - ABZ Conference, Orford, Quebec, Canada. (Submitted)
Gondal, Ali, Poppleton, Mike, Butler, Michael and Snook, Colin (2010) Feature-Oriented Modelling Using Event-B. International Conference on Software Engineering Theory and Practice (SETP-10), Orlando, FL., United States. 11 - 13 Jul 2010.
Yeganefard, Sanaz, Butler, Michael and Rezazadeh, Abdolbaghi (2010) Evaluation of a Guideline by Formal Modelling of Cruise Control System in Event-B. Proceedings of the Second NASA Formal Methods Symposium (NFM 2010), NASA/CP-2010-216215, Washington DC. 12 - 13 Apr 2010. pp. 182-191 .
Abrial, Jean-Raymond, Butler, Michael, Hallerstede, Stefan, Hoang, Thai Son, Mehta, Farhad and Voisin, Laurent (2010) Rodin: an open toolset for modelling and reasoning in Event-B. International Journal on Software Tools for Technology Transfer, 12 (6), 447-466. (doi:10.1007/s10009-010-0145-y).
Maamria, Issam and Butler, Michael (2010) Rewriting and Well-Definedness within a Proof System. Partiality and Recursion in Interactive Theorem Provers PAR-10.
Salehi Fathabadi, Asieh and Butler, Michael (2010) Applying Event-B Atomicity Decomposition to a Multi Media Protocol. FMCO Formal Methods for Components and Objects. pp. 89-104 . (doi:10.1007/978-3-642-17071-3_5).
Silva, Renato, Pascal, Carine, Hoang, Thai Son and Butler, Michael (2011) Decomposition Tool for Event-B. Software: Practice and Experience, 41 (2), 199-208. (doi:10.1002/spe.1002).
Gondal, Ali, Poppleton, Mike and Butler, Michael (2011) Composing Event-B Specifications - Case-Study Experience. Apel, S and Jackson, E (eds.) 10th International Conference on Software Composition, Zurich, Switzerland. 29 - 30 Jun 2011. pp. 100-115 .
Edmunds, Andrew and Butler, Michael (2011) Tasking Event-B: An Extension to Event-B for Generating Concurrent Code. PLACES 2011, Saarbrucken, Germany. (In Press)
Ireland, Andrew, Grov, Gudmund, Llano, Maria Teresa and Butler, Michael (2013) Reasoned modelling critics: turning failed proofs into modelling guidance. [in special issue: Abstract State Machines, Alloy, B and Z - Selected Papers from ABZ 2010] Science of Computer Programming, 78 (3), 293-309. (doi:10.1016/j.scico.2011.03.006).
Salehi Fathabadi, Asieh, Rezazadeh, Abdolbaghi and Butler, Michael (2011) Applying Atomicity and Model Decomposition to a Space Craft System in Event-B. THIRD NASA FORMAL METHODS SYMPOSIUM, Pasadena, California. 17 - 19 Apr 2011.
Silva, Renato and Butler, Michael (2010) Shared Event Composition/Decomposition in Event-B. FMCO Formal Methods for Components and Objects, Graz, Austria. 29 Nov - 01 Dec 2010.
Sarshogh, Mohammad Reza and Butler, Michael (2011) Specification and refinement of discrete timing properties in Event-B. AVoCS 2011, Newcastle. (Submitted)
Butler, Michael and Schulte, Wolfram (2011) FM 2011: Formal Methods - 17th International Symposium on Formal Methods, Limerick, Ireland, June 20-24, 2011 , Springer
Colley, John and Butler, Michael (2009) On Proving with Event-B that a Pipelined Processor Model Implements its ISA Specification. Dagstuhl Seminar on Refinement Based Methods for the Construction of Dependable Systems, Dagstuhl.
Edmunds, Andrew, Rezazadeh, Abdolbaghi and Butler, Michael (2011) From Event-B models to code: sensing, actuating, and the environment. SBMF2011, Sao Paulo, Brazil. 25 - 27 Sep 2011. 6 pp .
Snook, Colin, Savicks, Vitaly and Butler, Michael (2011) Verification of UML models by translation to UML-B. Lecture Notes in Computer Science, 6957, 251.
Edmunds, Andrew, Rezazadeh, Abdolbaghi and Butler, Michael (2012) Formal modelling for Ada implementations: tasking Event-B. Ada-Europe 2012: 17th International Conference on Reliable Software Technologies, Stockholm, Sweden. 10 - 14 Jun 2012. 14 pp .
Edmunds, Andrew, Butler, Michael, Maamria, Issam, Silva, Renato and Lovell, Chris (2012) Event-B code generation: type extension with theories. ABZ 2012, Pisa, Italy. 18 - 20 Jun 2012. 4 pp .
Yeganefard, Sanaz and Butler, Michael (2012) Control systems: phenomena and structuring functional requirement documents. 17th IEEE International Conference on Engineering of Complex Computer Systems (ICECCS 2012)., Paris, France. 17 - 19 Jul 2012. 10 pp . (Submitted)
Yeganefard, Sanaz and Butler, Michael (2011) Structuring functional requirements of control systems to facilitate refinement-based formalisation. [in special issue: Automated Verification of Critical Systems 2011] Electronic Communications of the EASST, 46.
Lovell, Chris, Edmunds, Andy, Silva, Renato, Maamria, Issam and Butler, Michael (2012) Ensuring extensibility within code generation. Rodin User and Developer Workshop, Fontainebleau, France. 27 - 29 Feb 2012.
Edmunds, Andrew, Lovell, Chris, Silva, Renato, Maamria, Issam and Butler, Michael (2012) Code generation update. Rodin User and Developer Workshop, Fontainebleau, France. 27 - 29 Feb 2012. 2 pp .
Butler, Michael, Salehi Fathabadi, Asieh and Silva, Renato (2012) Event-B and Rodin. In, Boulanger, Jean-Louis (ed.) Industrial Use of Formal Methods: Formal Verification. Chichester, GB. ISTE; Wiley, pp. 215-245.
Salehi Fathabadi, Asieh, Butler, Michael and Rezazadeh, Abdolbaghi (2012) A systematic approach to atomicity decomposition in Event-B. [in special issue: Software Engineering and Formal Methods. 10th International Conference, SEFM 2012, Thessaloniki, Greece, October 1-5, 2012. Proceedings] Lecture Notes in Computer Science, 7504, 78-93. (doi:10.1007/978-3-642-33826-7_6).
Butler, Michael (2012) External and internal choice with event groups in Event-B. [in special issue: Celebrating the 60th Birthday of Carroll Morgan] Formal Aspects of Computing, 24 (4-6), 555-567. (doi:10.1007/s00165-012-0239-2).
Edmunds, Andrew, Colley, John and Butler, Michael (2012) Building on the DEPLOY legacy: code generation and simulation. DS-Event-B-2012: Workshop on the experience of and advances in developing dependable systems in Event-B.
Said, Mar Yah (2012) ATM Case study models - UML-B/Event-B. University of Southampton [Dataset]
Butler, Michael (2013) Mastering System Analysis and Design through Abstraction and Refinement. In, Engineering Dependable Software Systems. Summer School on Engineering Dependable Software Systems, Marktoberdorf, Germany, 2012 (01/01/13) IOS Press.
Satpathy, Manoranjan, Snook, Colin, Arora, Silky, Ramesh, S and Butler, Michael (2013) Systematic Development of Control Designs via Formal Refinement. International Conference on Model-Driven Engineering and Software Development.
Colley, John and Butler, Michael (2013) A Formal, Systematic Approach to STPA using Event-B Refinement and Proof. 21th Safety Critical System Symposium.
Butler, Michael, Colley, John, Edmunds, Andrew, Snook, Colin, Evans, Neil, Grant, Neil and Marshall, Helen (2013) Modelling and Refinement in CODA. Refine. pp. 36-51 .
Satpathy, M., Ramesh, S., Snook, Colin, Singh, N.K. and Butler, Michael (2013) A Mixed Approach to Rigorous Development of Control Designs. IEEE Multi-Conference on Systems and Control (MSC 2013).
Butler, Michael and Maamria, Issam (2013) Practical Theory Extension in Event-B. Festschrift Symposium in Honour of He Jifeng on the Occasion of His 70th Birthday.
Yeganefard, Sanaz and Butler, Michael (2013) Problem Decomposition and Sub-Model Reconciliation of Control Systems in Event-B. IEEE International Workshop on Formal Methods Integration.
Banach, Richard and Butler, Michael (2013) Cruise Control in Hybrid Event-B. International Colloquium on Theoretical Aspects of Computing (ICTAC).
Banach, Richard and Butler, Michael (2013) A Hybrid Event-B Study of Lane Centering. Complex Systems Design & Management (CSD&M) 2013.
Dghaym, Dana, Butler, Michael and Salehi Fathabadi, Asieh (2014) Evaluation of graphical control flow management approaches for Event-B modelling. Proceedings of the 13th International Workshop on Automated Verification of Critical Systems (AVocS 2013), Guildford, United Kingdom. 15 pp . (doi:10.14279/tuj.eceasst.66.891).
Bicknell, Brett, Reis, Jose, Butler, Michael, Colley, John and Snook, Colin (2012) A Practical Approach for Closed Systems Formal Verification Using Event-B. 10th International Conference on Software Engineering and Formal Methods (SEFM 2012). pp. 323-332 .
Butler, Michael, Voisin, Laurent and Muller, Thomas (2013) Tooling in DEPLOY. In, Romanovsky, Alexander and Thomas, Martin (eds.) Industrial Deployment of System Engineering Methods. Springer.
Said, Mar Yah, Butler, Michael and Snook, Colin (2015) A method of refinement in UML-B. Software and Systems Modeling, 14 (4), 1557–1580. (doi:10.1007/s10270-013-0391-z).
Alkhammash, Eman, Salehi Fathabadi, Asieh, Butler, Michael and Cirstea, Corina (2013) Building Traceable Event-B Models from Requirements. Automated Verification of Critical Systems (AVoCS 2013).
Savicks, Vitaly, Butler, Michael, Bendisposto, Jens and Colley, John (2013) Co-simulation of Event-B and Continuous Models in Rodin. 4th Rodin User and Developer Workshop.
Pereverzeva, Inna, Butler, Michael and Salehi Fathabadi, Asieh et al. (2014) Formal derivation of distributed MapReduce. 4th International ABZ 2014 Conference, , Toulouse, France. 01 - 05 Jun 2014. 17 pp .
Chaudemar, Jean-Charles, Savicks, Vitaly, Butler, Michael and Colley, John (2014) Co-simulation of Event-B and Ptolemy II Models via FMI. Embedded Real-time software and systems (ERTSS 2014).
Reis, Jose, Bicknell, Brett, Butler, Michael and Colley, John (2014) Innovative Approach for Requirements Verification of Closed Systems. Embedded Real-time software and systems (ERTSS 2014).
Savicks, Vitaly, Butler, Michael and Colley, John (2014) Co-simulation environment for Rodin: landing gear case study. 4th International ABZ 2014 Conference, , Toulouse, France. 01 - 05 Jun 2014. (doi:10.1007/978-3-319-07512-9_11).
Savicks, Vitaly, Butler, Michael, Colley, John and Bendisposto, Jens (2014) Rodin multi-simulation plug-in. 5th Rodin User and Developer Workshop, Toulouse, Toulouse, France. 01 - 02 Jun 2014.
Savicks, Vitaly, Butler, Michael and Colley, John (2014) Co-simulating Event-B and continuous models via FMI. 2014 Summer Computer Simulation Conference, Monterey, United States. 05 - 09 Jul 2014.
Salehi Fathabadi, Asieh, Snook, Colin and Butler, Michael (2014) Applying an integrated modelling process to run-time management of many-core systems. 11th International Conference on Integrated Formal Methods (iFM), Bertinoro, Italy. 08 - 10 Sep 2014.
Salehi Fathabadi, Asieh, Butler, Michael and Rezazadeh, Abdolbaghi (2015) Language and tool support for event refinement structures in Event-B. Formal Aspects of Computing, 27 (3), 499-523. (doi:10.1007/s00165-014-0311-1).
Dalvandi, Mohammadsadegh, Butler, Michael and Rezazadeh, Abdolbaghi (2015) From Event-B models to Dafny code contracts. 6th IPM International Conference on Fundamentals of Software Engineering, Tehran, Iran, Islamic Republic of. 21 - 23 Apr 2015.
Butler, Michael, Abrial, Jean-Raymond and Banach, Richard (2016) Modelling and Refining Hybrid Systems in Event-B and Rodin. In, Petre, Luigia and Sekerinski, Emil (eds.) From Action System to Distributed Systems: The Refinement Approach. Taylor & Francis. (doi:10.1201/b20053-5).
Alkhammash, Eman, Butler, Michael, Fathabadi, Asieh Salehi and Cîrstea, Corina (2015) Building traceable Event-B models from requirements. Science of Computer Programming, 1- 21. (doi:10.1016/j.scico.2015.06.002).
Banach, Richard, Butler, Michael, Qin, Shengchao, Verma, Nitika and Zhu, Huibiao (2015) Core Hybrid Event-B I: Single Hybrid Event-B machines. Science of Computer Programming, 105, 92-123. (doi:10.1016/j.scico.2015.02.003).
Eleftherakis, George, Butler, Michael and Hinchey, Mike (2015) Editorial. Formal Asp. Comput., 27 (3), 473. (doi:10.1007/s00165-015-0335-1).
Wilkinson, Toby, Butler, Michael and Colley, John (2014) A Systematic Approach to Requirements Driven Test Generation for Safety Critical Systems. Model-Based Safety and Assessment - 4th International Symposium, {IMBSA} 2014, Munich, Germany, October 27-29, 2014. Proceedings. pp. 43-56 . (doi:10.1007/978-3-319-12214-4_4).
Salehi Fathabadi, Asieh, Maeda-Nunez, Luis Alfonso, Butler, Michael, Al-Hashimi, Bashir and Merrett, Geoff (2015) Towards automatic code generation of run-time power management for embedded systems using formal methods. 9th International Symposium on Embedded Multicore/Many-core Systems-on-Chip (MCSoC-15), Turin, Italy. 22 - 24 Sep 2015. 8 pp .
Dalvandi, Mohammadsadegh, Butler, Michael and Rezazadeh, Abdolbaghi (2015) Transforming Event-B models to Dafny contracts. 15th International Workshop on Automated Verification of Critical Systems (AVoCS 2015), Edinburgh, United Kingdom. 31 Aug - 03 Sep 2015.
Wilkinson, Toby, Butler, Michael, Paxton, Martin and Waldron, Xanthippe (2015) A Formal Approach to Multi-UAV Route Validation. Fourth International Workshop on Formal Techniques for Safety-Critical Systems.
Butler, Michael (2016) Lectures on Modelling and Verification in Event-B. Spring School on Engineering Trustworthy Software Systems 2016, Chongqinq, China.
Dghaym, Dana, Trindade, Matheus Garay, Butler, Michael and Salehi Fathabadi, Asieh (2016) A graphical tool for event refinement structures in Event-B. Abstract State Machines, Alloy, B, TLA, VDM, and Z: Proceedings of the 5th International Conference, ABZ 2016, Linz, Austria, May 23-27, 2016, Linz, Austria. pp. 269-274 . (doi:10.1007/978-3-319-33600-8_20).
Hoang, Thai Son, Snook, Colin, Ladenberger, Lukas and Butler, Michael (2016) Validating the requirements and design of a hemodialysis machine using iUML-B, BMotion Studio, and co-simulation. Abstract State Machines, Alloy, B, TLA, VDM, and Z - 5th International Conference, ABZ 2016, Linz, Austria, May 23-27, 2016, Proceedings. pp. 360-375 . (doi:10.1007/978-3-319-33600-8_31).
Darbari, Ashish, Singleton, Iain, Butler, Michael and Colley, John (2016) Formal modelling, testing and verification of HSA memory models using Event-B Southampton, GB. University of Southampton 9pp.
Hoang, Thai Son, Snook, Colin, Ladenberger, Lukas and Butler, Michael (2016) Formal specification of a Haemodialysis Machine (HD Machine) using Event-B. University of Southampton [Dataset]
Butler, Michael (2017) Reasoned modelling with Event-B. In, Bowen, Jonathan P., Liu, Zhiming and Zhang, Zili (eds.) Engineering Trustworthy Software Systems. (Lecture Notes in Computer Science, 10215) Heidelberg, DE. Springer, pp. 51-109. (doi:10.1007/978-3-319-56841-6).
Al-Brashdi, Ahmed, Butler, Michael, Rezazadeh, Abdolbaghi and Snook, Colin (2016) Tool support for model-based database design with Event-B. Ogata, K, Lawford, M and Liu, S (eds.) In Formal Methods and Software Engineering: ICFEM 2016. vol. 10009, Springer. pp. 210-225 . (doi:10.1007/978-3-319-47846-3_14).
Banach, Richard and Butler, Michael (2016) Modelling hybrid systems in Event-B and Hybrid Event-B: a comparison of water tanks. Formal Methods and Software Engineering - 18th International Conference on Formal Engineering Methods, {ICFEM} 2016, Proceedings, Tokyo, Japan. 14 - 18 Nov 2016. pp. 90-105 . (doi:10.1007/978-3-319-47846-3_7).
Alkhammash, Eman, Butler, Michael and Cirstea, Corina (2016) Modeling guidelines of FreeRTOS in Event-B. Communication, Management and Information Technology: Proceedings of the International Conference on Communication, Management and Information Technology (Iccmit 2016). pp. 453-462 .
Salehi Fathabadi, Asieh, Butler, Michael and Snook, Colin (2016) Extending Code Generation to Support Platform-Independent Event-B Models. Rodin Developer Workshop, 2016. p. 21 .
Snook, Colin, Hoang, Thai Son and Butler, Michael (2016) iUML-B model of VLAN system. University of Southampton doi:10.5258/SOTON/403533 [Dataset]
Banach, Richard, Butler, Michael, Qin, Shengchao and Zhu, Huibao (2017) Core Hybrid Event-B II: Multiple cooperating Hybrid Event-B machines. Science of Computer Programming, 139, 1-35. (doi:10.1016/j.scico.2016.12.003).
Hoang, Son, Voisin, Laurent, Salehi Fathabadi, Asieh, Butler, Michael, Wilkinson, Toby and Beauger, Nicolas (2017) Theory plug-in for Rodin 3.x. arXiv, abs/1701.08625, 1-9.
Hoang, Thai Son, Salehi Fathabadi, Asieh, Butler, Michael and Voisin, Laurent (2016) Theory plug-in for Rodin 3.x. 6th Rodin User and Developer Workshop, Linz, Austria. 22 May 2016. 2 pp .
Howard, Giles, Butler, Michael, Colley, John and Sassone, Vladimiro (2017) Formal analysis of safety and security requirements of critical systems supported by an extended STPA methodology. 2nd Workshop on Safety & Security aSSurance, , Paris, France. 29 Apr 2017. 6 pp . (In Press) (doi:10.1109/EuroSPW.2017.68).
Snook, Colin, Hoang, Thai Son and Butler, Michael (2017) Analysing security protocols using refinement in iUML-B. In, Barrett, Clark, Davies, Misty and Kahsai, Temesghen (eds.) NASA Formal Methods: 9th International Symposium, NFM 2017, Moffett Field, CA, USA, May 16-18, 2017, Proceedings. (Lecture Notes in Computer Science, 10227) 9th NASA Formal Methods Symposium (15/05/17 - 18/05/17) Springer, pp. 84-98. (doi:10.1007/978-3-319-57288-8_6).
Dalvandi, Mohammad Sadegh, Butler, Michael and Rezazadeh, Abdolbaghi (2017) Derivation of algorithmic control structures in Event-B refinement. Science of Computer Programming, 148, 49-65, [SCICO2103]. (doi:10.1016/j.scico.2017.05.010).
Hoang, Thai Son, Snook, Colin, Dghaym, Dana and Butler, Michael (2017) Class diagrams for Abstract Data Types. Hung, D. and Kapur, D. (eds.) In Theoretical Aspects of Computing – ICTAC 2017. vol. 10580, Springer. pp. 100-117 . (doi:10.1007/978-3-319-67729-3_7).
Butler, Michael, Dghaym, Dana, Fischer, Tomas, Hoang, Thai Son, Reichl, Klaus, Snook, Colin and Tummeltshammer, Peter (2017) Formal modelling techniques for efficient development of railway control products. Fantechi, A., Lecomte, T. and Romanovsky, A. (eds.) In RSSRail 2017 : Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification. vol. 10598, Springer.. (doi:10.1007/978-3-319-68499-4_5).
Hoang, Thai, Snook, Colin, Dghaym, Dana and Butler, Michael (2017) RailGround using Theory plug-in. University of Southampton doi:10.5258/SOTON/D0162 [Dataset]
Bogdiukiewicz, Chris, Butler, Michael, Hoang, Thai Son, Paxton, Martin, Snook, James, Harvey, Waldron, Xanthippe and Wilkinson, Toby (2017) Formal development of policing functions for intelligent systems. In 2017 IEEE 28th International Symposium on Software Reliability Engineering (ISSRE). IEEE. 11 pp . (doi:10.1109/ISSRE.2017.40).
Snook, Colin, Dghaym, Dana, Hoang, Thai Son, Butler, Michael, Reichl, Klaus, Fischer, Tomas and Tummeltshammer, Peter (2017) Railground RSSRail models - iUML-B/Event-B. University of Southampton doi:10.5258/SOTON/D0184 [Dataset]
Bogdiukiewicz, Chris, Butler, Michael, Hoang, Thai Son, Paxton, Martin, Snook, James, Harvey, Waldron, Xanthippe and Wilkinson, Toby (2017) Route Validation in Event-B. University of Southampton doi:10.5258/SOTON/D0217 [Dataset]
Hoang, Thai Son, Dghaym, Dana, Snook, Colin and Butler, Michael (2018) A composition mechanism for refinement-based methods. In Proceedings 2017 22nd International Conference on Engineering of Complex Computer Systems: ICECCS 2017. IEEE. 10 pp . (doi:10.1109/ICECCS.2017.27).
Dghaym, Dana, Butler, Michael and Salehi Fathabadi, Asieh (2018) Extending ERS for modelling dynamic workflows in Event-B. 22nd International Conference on Engineering of Complex Computer Systems, The Kyushu University, Fukuoka, Japan. 05 - 08 Nov 2017. pp. 20-29 . (doi:10.1109/ICECCS.2017.29).
Hoang, Thai Son, Dghaym, Dana, Snook, Colin and Butler, Michael (2017) Development of a System Controlling Cars on a Bridge using Machine Inclusion. University of Southampton doi:10.5258/SOTON/D0237 [Dataset]
Hoang, Thai Son, Snook, Colin, Salehi Fathabadi, Asieh, Butler, Michael and Ladenberger, Lukas (2017) Validating and verifying the requirements and design of a haemodialysis machine using the rodin toolset. Science of Computer Programming. (doi:10.1016/j.scico.2017.11.002).
Al-Brashdi, Ahmed, Zahran Nasser, Butler, Michael and Rezazadeh, Abdolbaghi (2018) Incremental database design using UML-B and Event-B. 2nd Workshop on Formal and Model-Driven Techniques for Developing Trustworthy Systems, , Xi'an, China. 16 Nov 2017. pp. 34-47 . (doi:10.4204/EPTCS.271.3).
Salehi Fathabadi, Asieh, Butler, Michael J., Yang, Sheng, Maeda-Nunez, Luis, Bantock, James, Al-Hashimi, Bashir M. and Merrett, Geoff V. (2018) A model-based framework for software portability and verification in embedded power management systems. Journal of Systems Architecture, 82, 12-23. (doi:10.1016/j.sysarc.2017.12.001).
Zhu, Chenyang, Butler, Michael and Cirstea, Corina (2018) Refinement of timing constraints for concurrent tasks with scheduling. Butler, M., Raschke, A., Hoang, T. and Reichl, K. (eds.) In Abstract State Machines, Alloy, B, TLA, VDM, and Z: ABZ 2018. vol. 10817, Springer. pp. 219-233 . (doi:10.1007/978-3-319-91271-4).
Dalvandi, Mohammad Sadegh, Butler, Michael, Rezazadeh, Abdolbaghi and Salehi Fathabadi, Asieh (2018) Verifiable code generation from scheduled event-B models. In Abstract State Machines, Alloy, B, TLA, VDM, and Z: ABZ 2018. vol. 10817, Springer. pp. 1-15 . (doi:10.1007/978-3-319-91271-4_16).
Dalvandi, Mohammad Sadegh, Salehi Fathabadi, Asieh and Butler, Michael (2018) Using formal methods for automatic platform-independent code generation of run-time management. University Booth at DATE 2018, Maritim Hotel & Internationales Congress Center, Dresden, Germany. 19 - 22 Mar 2018.
Dalvandi, Mohammad Sadegh and Butler, Michael (2014) Towards verified implementation of Event-B models in Dafny. 5th Rodin User and Developer Workshop, Toulouse, Toulouse, France. 01 - 02 Jun 2014.
Butler, Michael and Schewe, Klaus Dieter (2018) Introduction to the ABZ 2016 Special issue. Science of Computer Programming. (doi:10.1016/j.scico.2018.01.005).
Dalvandi, Mohammad Sadegh, Salehi Fathabadi, Asieh and Butler, Michael (2018) A report on PRiME code generation activities. 7th Rodin Workshop, , Southampton, United Kingdom. 04 Jun 2018.
Zhu, Chenyang, Butler, Michael and Cirstea, Corina (2018) Semantics of real-time trigger-response properties in Event-B. In 2018 International Symposium on Theoretical Aspects of Software Engineering (TASE). IEEE. pp. 150-156 . (doi:10.1109/TASE.2018.00028).
Al-Brashdi, Ahmed, Zahran Nasser, Butler, Michael and Rezazadeh, Abdolbaghi (2018) UB2DB Rodin plug-in for automated database code generation. 7th Rodin Workshop, , Southampton, United Kingdom. 04 Jun 2018. pp. 1-2 .
Hoang, Thai Son, Sato, Naoto, Myosin, Tomoyuki, Butler, Michael, Nakagawa, Yuichiroh and Ogawa, Hideto (2018) Policing functions for machine learning systems. Workshop on Verification and Validation of Autonomous Systems: Satellite Workshop of Floc 2018, University of Oxford, Oxford, United Kingdom. 18 - 19 Jul 2018. 10 pp . (In Press)
Hoang, Thai Son, Butler, Michael and Reichl, Klaus (2018) The hybrid ERTMS/ETCS level 3 case study. In Abstract State Machines, Alloy, B, TLA, VDM, and Z - 6th International Conference, ABZ 2018, Proceedings. vol. 10817 LNCS, Springer Verlag. pp. 251-261 . (doi:10.1007/978-3-319-91271-4_17).
Hoang, Thai Son and Butler, Michael (2018) Rodin Developments for Formal Policing Functions based on Metamorphic Relations. University of Southampton doi:10.5258/SOTON/D0528 [Dataset]
Snook, James, Harvey, Butler, Michael and Hoang, Thai Son (2018) Developing a new language to construct algebraic hierarchies for Event-B. In Dependable Software Engineering. Theories, Tools, and Applications: SETTA 2018. vol. 10998, Springer. pp. 135-141 . (doi:10.1007/978-3-319-99933-3_9).
Snook, Colin, Hoang, Thai Son, Dghaym, Dana, Butler, Michael, Fischer, Tomas, Schlick, Rupert and Wang, Keming (2018) Behaviour-driven formal model development. Sun, J. and Sun, M. (eds.) In Formal Methods and Software Engineering: 20th International Conference on Formal Engineering Methods, ICFEM 2018, Gold Coast, QLD, Australia, November 12-16, 2018, Proceedings. Springer. pp. 21-36 . (doi:10.1007/978-3-030-02450-5_2).
Morris, Karla, Snook, Colin, Hoang, Thai Son, Armstrong, Robert and Butler, Michael (2018) Refinement of statecharts with run-to-completion semantics. The Sixth International Workshop on Formal Techniques for Safety-Critical Systems, , Gold Coast, Australia. 16 Nov 2018.
Butler, Michael, Raschke, Alexander, Hoang, Thai Son and Reichl, Klaus (2018) Preface. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 10817, III-VI.
Dghaym, Dana, Snook, Colin, Hoang, Thai Son and Butler, Michael (2018) Reusing formal models via lifting. In Proceedings - 23rd International Conference on Engineering of Complex Computer Systems, ICECCS 2018. vol. 2018-December, Institute of Electrical and Electronics Engineers Inc. pp. 189-192 . (doi:10.1109/ICECCS2018.2018.00029).
Sato, Naoto, Kuruma, Hironobu, Kaneko, Masanori, Nakagawa, Yuichiroh, Ogawa, Hideto, Hoang, Thai Son and Butler, Michael (2018) DeepSaucer: Unified environment for verifying Deep Neural Networks. arXiv.
Howard, Giles, Butler, Michael, Colley, John and Sassone, Vladimiro (2019) A methodology for assuring the safety and security of critical infrastructure based on STPA and Event-B. International Journal of Critical Computer-Based Systems, 56-75. (doi:10.1504/IJCCBS.2019.098815).
Omitola, Temitope, Downes, Jonathan, Wills, Gary, Zwolinski, Mark and Butler, Michael (2018) Securing navigation of unmanned maritime systems. Schillai, Sophia M. and Townsend, Nicholas C. (eds.) In Proceedings of the 11th International Robotic Sailing Conference: Southampton, United Kingdom, August 31st - September 1st, 2018. vol. 2331, CEUR-WS. pp. 53-62 .
Zhu, Chenyang, Butler, Michael and Cirstea, Corina (2019) Towards refinement semantics of real-time trigger-response properties in Event-B. 13th International Symposium on Theoretical Aspects of Software Engineering, Guilin, Guilin, China. 29 Jul - 01 Aug 2019. 8 pp .
Salehi Fathabadi, Asieh, Dalvandi, Mohammad Sadegh and Butler, Michael (2019) Developing portable embedded software for multicore systems through formal abstraction and refinement. In, Al-Hashimi, Bashir M. and Merrett, Geoff V. (eds.) Many-Core Computing: Hardware and Software. Institute of Engineering and Technology, IET.
Snook, Colin, Hoang, Thai Son, Dghaym, Dana and Butler, Michael (2019) Domain-specific scenarios for refinement-based methods. Attiogbe, C., Ferrarotti, F. and Maabout, S. (eds.) In DETECT 2019: moDeling, vErification and Testing of dEpendable CriTical systems. Springer. pp. 18-31 . (doi:10.1007/978-3-030-32213-7_2).
Omitola, Temitope, Butler, Michael and Rezazadeh, Abdolbaghi (2019) Making (implicit) security requirements explicit for cyber-physical systems: A maritime use case security analysis. Anderst-Kotsis, G., Tjoa, A. and Khalil, I. (eds.) In Database and Expert Systems Applications. vol. 1062, Springer. pp. 75-84 . (doi:10.1007/978-3-030-27684-3_11).
Zhu, Chenyang (2019) Dataset for 'Formalizing Hierarchical Scheduling for Refinement of Real-Time Systems'. University of Southampton doi:10.5258/SOTON/D1075 [Dataset]
Dghaym, Dana, Turnock, Stephen, Butler, Michael, Downes, Jonathan, Hoang, Thai Son and Pritchard, Ben (2019) Developing a framework for trustworthy autonomous maritime systems. Valdez Banda, Osiris Alejandro, Kujala, Pentti, Hirdaris, Spyros and Basnet, Sunil (eds.) In Proceedings of the International Seminar on Safety and Security of Autonomous Vessels (ISSAV) and European STAMP Workshop and Conference (ESWC) 2019: ISSAV 2019. Sciendo. pp. 73-82 . (doi:10.2478/9788395669606-007).
Butler, Michael, Dghaym, Dana, Hoang, Thai Son, Omitola, Temitope, Snook, Colin, Fellner, Andreas, Schlick, Rupert, Tarrach, Thorsten, Fischer, Tomas and Tummeltshammer, Peter (2019) Behaviour-driven formal model development of the ETCS hybrid level 3. In The 24th International Conference on Engineering Of Complex Computer Systems: ICECCS 2019. pp. 1-10 . (In Press)
Dalvandi, Mohammad Sadegh, Butler, Michael and Salehi Fathabadi, Asieh (2019) SEB-CG: Code generation tool with algorithmic refinement support for Event-B. Practical Formal Verification for Software Dependability: co-located with the Formal Methods 2019 (FM'19), , Porto, Portugal. 07 Oct 2019.
Salehi Fathabadi, Asieh, Dalvandi, Mohammadsadegh, Butler, Michael and Al-Hashimi, Bashir M. (2019) Verifying cross-layer interactions through formal model-based assertion generation. IEEE Embedded Systems Letters. (doi:10.1109/LES.2019.2955316).
Zhu, Chenyang, Butler, Michael and Cirstea, Corina (2020) Formalizing hierarchical scheduling for refinement of real-time systems. Science of Computer Programming, 189, [102390]. (doi:10.1016/j.scico.2020.102390).
Zhu, Chenyang, Butler, Michael and Cirstea, Corina (2020) Real-time trigger-response properties for Event-B applied to the pacemaker. In The 14th International Symposium on Theoretical Aspects of Software Engineering. IEEE. 8 pp . (In Press)
Butler, Michael, Hoang, Thai Son, Raschke, Alexander and Reichl, Klaus (2020) Introduction to special section on the ABZ 2018 case study: Hybrid ERTMS/ETCS Level 3. International Journal on Software Tools for Technology Transfer, 22 (3), 249-255. (doi:10.1007/s10009-020-00562-3).
Fischer, Tomas, Reichl, Klaus, Tummeltshammer, Peter, Hoang, Thai Son and Butler, Michael (2020) Validation of railway control systems. In, Leitner, A., Watzenig, D. and Ibanez-Guzman, J. (eds.) Validation and Verification of Automated Systems. (HASH(0xd25dda8)) Cham. Springer International Publishing, pp. 221-229. (doi:10.1007/978-3-030-14628-3_17).
Zhu, Chenyang, Butler, Michael and Cirstea, Corina (2020) Trace semantics and refinement patterns for real-time properties in event-B models. Science of Computer Programming, 197, [102513]. (doi:10.1016/j.scico.2020.102513).
Snook, Colin, Hoang, Thai Son, Dghaym, Dana, Butler, Michael and Salehi Fathabadi, Asieh (2020) Dataset for: Domain-Specific Scenarios for Refinement-based Methods. University of Southampton doi:10.5258/SOTON/D1026 [Dataset]
Snook, Colin, Hoang, Thai Son, Dghaym, Dana, Salehi Fathabadi, Asieh and Butler, Michael (2021) Domain-specific scenarios for refinement-based methods. Journal of Systems Architecture, 112, [101833].
Hoang, Thai Son, Voisin, Laurent and Butler, Michael (2020) Domain-specific developments using Rodin theories. In, Ait-Ameur, Yamine, Nakajima, Shin and Méry, Dominique (eds.) Implicit and Explicit Semantics Integration in Proof Based Developments of Discrete Systems: Communications of NII Shonan Meetings. Springer Nature.
Morris, Karla, Snook, Colin, Hoang, Thai Son, Hulette, G., Armstrong, Robert and Butler, Michael (2020) Formal verification of run-to-completion style statecharts using Event-B. Muccini, Henry, Avgeriou, Paris, Buhnova, Barbora, Camara, Javier, Caporuscio, Mauro, Franzago, Mirco, Koziolek, Anne, Scandurra, Patrizia, Trubiani, Catia, Weyns, Danny and Zdun, Uwe (eds.) In Software Architecture. ECSA 2020.: Communications in Computer and Information Science. vol. 1269, Springer, Cham. pp. 311-325 . (doi:10.1007/978-3-030-59155-7_24).
Dghaym, Dana, Hoang, Thai Son, Turnock, Stephen, Butler, Michael, Downes, Jon and Pritchard, Ben (2021) An STPA-based formal composition framework for trustworthy autonomous maritime systems. Safety Science, 136 (0925-7535), [105139].
Hoang, Thai Son, Snook, Colin, Dghaym, Dana, Salehi Fathabadi, Asieh and Butler, Michael (2021) The CamilleX Framework for the Rodin Platform. ABZ 2021- 8th International Conference on Rigorous State Based Methods: ABZ 2021, virtual. 07 - 11 Jun 2021. pp. 124-129 .
Salehi Fathabadi, Asieh, Snook, Colin, Hoang, Thai Son, Dghaym, Dana and Butler, Michael (2021) Extensible Record Structures in Event-B. ABZ 2021- 8th International Conference on Rigorous State Based Methods: ABZ 2021, virtual. 07 - 11 Jun 2021. pp. 130-136 .
Dghaym, Dana, Hoang, Thai Son, Butler, Michael, Hu, Runshan, Aniello, Leonardo and Sassone, Vladimiro (2021) Verifying System-level Security of a Smart Ballot Box. In ABZ 2021 – 8th International Conference on Rigorous State Based Methods: ABZ 2021. Springer Nature Switzerland AG. 16 pp . (In Press)
Zhu, Chenyang, Butler, Michael, Cirstea, Corina and Hoang, Thai Son (2021) Reasoning About Real-Time Systems in Event-B Models with Fairness Assumptions. In Proceedings of TASE2021 Conference. (In Press)
Salehi Fathabadi, Asieh, Snook, Colin, Hoang, Thai Son, Dghaym, Dana and Butler, Michael (2021) Refinable record structures in formal methods. The International Workshop DETECT 2021. pp. 3-15 .
Hoang, Thai Son, Snook, Colin, Salehi Fathabadi, Asieh, Dghaym, Dana and Butler, Michael (2021) Towards CamilleX 3.0. 9th Rodin User and Developer Workshop, virtual. 08 - 11 Jun 2021.
Snook, Colin, Hoang, Thai Son, Salehi Fathabadi, Asieh, Dghaym, Dana and Butler, Michael (2021) Scenario Checker: An Event-B tool for validating abstract models. 9th Rodin User and Developer Workshop, virtual. 08 - 11 Jun 2021.