Michael Butler - Publications

Volumes

Integrated Formal Methods. Michael Butler, Luigia Petre, Kaisa Sere (Eds.). Integrated Formal Methods, LNCS 2335, Springer 2002.

Journals

Performance Analysis of Probabilistic Action Systems. Stefan Hallerstede and Michael Butler. Formal Aspects of Computing, To appear, 2004.
Extending the Concept of Transaction Compensation. Mandy Chessell, Catherine Griffin, David Vines, Michael Butler, Carla Ferreira, Peter Henderson. IBM Systems Journal, Vol. 41, No. 4, 743-758, 2002.
On the Use of Data Refinement in the Development of Secure Communications Systems. Michael Butler. Formal Aspects of Computing. Vol. 14, No. 1, pages 2-34, 2002.
A System-based Approach to the Formal Development of Embedded Controllers for a Railway. Michael Butler. Design Automation for Embedded Systems. Volume 6, Issue 4, 355-366, July 2002, ISSN 0929-5585
csp2B: A Practical Approach To Combining CSP and B. Michael Butler. Formal Aspects of Computing. Vol. 12, 182-196. 2000.
Reasoning about Grover's Quantum Search Algorithm using Probabilistic wp. Michael Butler and Pieter Hartel. ACM Transactions on Programming Languages and Systems. Volume 21 Issue 3 (1999):417-430, ISSN 0164-0925.
Calculational Derivation of Pointer Algorithms from Tree Operations. M. J. Butler. Science of Computer Programming. Vol. 33 Issue 3 (1999):221-260, ISSN 0167-6423.
Fusion and Simultaneous Execution in the Refinement Calculus. R.J.R Back and M.J. Butler. Acta Informatica. Vol. 35 Issue 11 (1998):921-949, ISSN 0001-5903.
Review of "The B-Book" by J.-R. Abrial. M. J. Butler. The Computer Journal, Vol.40.1 (1997):59-61, ISSN 0010-4620.
Stepwise Refinement of Communicating Systems. M. J. Butler. Science of Computer Programming, Vol. 27 (1996):139-173, ISSN 0167-6423.
Action Systems, Unbounded Nondeterminism, and Infinite Traces. M.J. Butler and C.C. Morgan. Formal Aspects of Computing, Vol. 7 (1995):37-53, ISSN 0934-5043.

Conferences and Collections

ProTest: An Automatic Test Environment for B Specifications. Satpathy, M., Leuschel, M. and Butler, M. Proceedings of International workshop on Model Based Testing, 2004.
The Use of Formal Methods in the Analysis of Trust (Position Paper). Butler, M., Leuschel, M., Lo Presti, S. and Turner, P. In Proceedings of Second International Conference on Trust Management (iTrust 2004) LNCS 2995 , pages pp. 333-339, Oxford, UK. Jensen, C., Poslad, S. and Dimitrakos, T., Eds.
An Operational Semantics for StAC, a Language for Modelling Long-running Business Transactions. Michael Butler and Carla Ferreira. Coordination 2004, Pisa.
Towards Formalizing UML State Diagrams in CSP. Muan Yong Ng and Michael Butler. Intl. Conf. on Formal Methods and Software Engineering, Brisbane, September 22-27, 2003.
ProB: A Model-Checker for B. Michael Leuschel and Michael Butler. FM 2003: 12th Intl. FME Symposium. Pisa, September 8-14, 2003.
Towards a Trust Analysis Framework for Pervasive Computing Scenarios. M Butler, M Leuschel, S Lo Presti, D Allsopp, P Beautement, C Booth, M Cusack and M Kirton. 6th Intl. Workshop on Trust, Privacy, Deception and Fraud in Agent Societies, in conjunction with AAMAS 2003.
Using SPIN and STeP to Verify StAC Specifications. Juan C. Augusto, Michael Butler, Carla Ferreira, and Stephen Craig. 5th International A.P.Ershov Conference on Perspectives of System Informatics (PSI'03). Novosibirsk, Russia. July 2003. Final Proceedings to be published in November.
Using Using the Extensible Model Checker XTL to Verify StAC Business Specifications. Juan C. Augusto, Michael Leuschel, Michael Butler and Carla Ferreira. 3rd Workshop on Automated Verification of Critical Systems (AVoCS 2003), pp. 253-266, Southampton (UK). April 2-3 2003.
Using B Refinement to Analyse Compensating Business Processes. Carla Ferreira and Michael Butler. ZB 2003: Formal Specification and Development in Z and B: Third International Conference of B and Z Users, Turku, Finland, Springer LNCS 2651, 2003.
Event-Based Modelling and Refinement of Distributed Monitoring and Control Systems. Abdolbaghi Rezazadeh and Michael Butler. Refinement of Critical Systems (RCS'03), Turku, June, 2003.
Tool Support For Visualizing CSP in UML. Muan Yong Ng and Michael Butler. Intl. Conf. on Formal Engineering Methods, Sanghai, October, 2002.
Tool Support For Visualizing CSP in UML. Muan Yong Ng and Michael Butler. AVoCS Workshop, Birmingham, UK, April, 2002.
An Approach to Modelling and Refining Timing Properties in B. Michael Butler and Jerome Falampin. Refinement of Critical Systems (RCS'02), Grenoble, January, 2002.
An Approach to Combining B and Alloy. Leonid Mikhailov and Michael Butler. Proc ZB'2002, Grenoble, January, 2002.
Animation and Model Checking of CSP and B using Prolog Technology. Michael Leuschel, Laksono Adhianto, Michael Butler, Carla Ferreira and Leonid Mikhailov (2001) Proceedings of the ACM Sigplan Workshop on Verification and Computational Logic VCL'2001 p.97-109.
Combining B and Alloy. Leonid Mikhailov and Michael Butler. Proc FMICS'01, Paris, July, 2001.
A Comparative Study of Formal and Informal Specifications through an Industrial Case Study. Manoranjan Satpathy, Rachel Harrison, Colin Snook and Michael Butler. In Dumke, Abran (Eds) Proc IEEE/ IFIP Workshop on Formal Specification of Computer Based Systems (FSCBS'01), 2001.
Using a Graphical Design Tool for Formal Specification. Colin Snook and Michael Butler. In Dumke, Abran (Eds) Proceedings 13th Annual Workshop of the Psychology of Programming Interest Group, 2001.
A Generic Model for Assessing Process Quality. Manoranjan Satpathy, Rachel Harrison, Colin Snook and Michael Butler. In Dumke, Abran (Eds) Proc International Workshop on Software Measurement (IWSM2000), Springer LNCS 2006, 2001.
Transacted Memory for Smart Cards. Michael Butler, Pieter Hartel, Eduard de Jong and Mark Longley . Formal Methods Europe (FME 2001), Berlin, March 2001.
Verifying Dynamic Properties of UML Models by Translation to the B Language and Toolkit. Michael Butler and Colin Snook. In ProceedingsUML 2000 WORKSHOP Dynamic Behaviour in UML Models: Semantic Questions, York, October 2000.
A Process Compensation Language. Michael Butler and Carla Ferreira. In W. Grieskamp T. Santen B. Stoddart (Eds.), Integrated Formal Methods (IFM 2000), Schloss Dagstuhl, Germany, November 2000. LNCS 1945, Springer, 2000, ISBN 3-540-41196-8.
Performing Algorithmic Refinement before Data Refinement in B. Michael Butler and Mairead Meagher. In Proceedings ZB2000, York, UK, September 2000. csp2B: A Practical Approach To Combining CSP and B. Michael Butler. In J. Wing, J. Woodcock, J. Davies (Eds.), FM'99 World Congress on Formal Methods, 20-24th Sept 1999, Toulouse, France, LNCS 1708, Springer, 1999, pp. 223-241, ISBN 3-540-66587-0.
Questions and Answers about Ten Formal Methods. Pieter Hartel, Michael Butler, Andrew Currie, Peter Henderson, Michael Leuschel, Andrew Martin, Adrian Smith, Ulrich Ultes-Nitsche, Bob Walters. In S. Gnesi, D. Latella (Eds), 4th Int. Workshop on Formal Methods for Industrial Critical Systems, Vol II (Trento, Italy, Jul 1999), ERCIM/CNR, Pisa, Italy, pp. 179-203, ISBN 88-7958-009-4.
Distributed electronic mail system. M.J. Butler. In Program Development by Refinement - Case Studies Using the B Method, Springer FACIT Series, Springer-Verlag, London 1999, pp. 301-322, ISBN 1-85233-053-8.
Parallel programming with the B method. M.J. Butler and M. Waldén. In Program Development by Refinement - Case Studies Using the B Method, Springer FACIT Series, Springer-Verlag, London 1999, pp. 183-195, ISBN 1-85233-053-8.
The operational semantics of a Java Secure Processor. P. H. Hartel, M. J. Butler, and M. Levy. In J. Alves-Foss, editor, Formal Syntax and Semantics of Java, LNCS 1523. Springer-Verlag, 1999.
Event Ordering in Action Systems. M.J. Butler. In J. Grundy, M. Schwenke, T. Vickers (Eds.), International Refinement Workshop / Formal Methods Pacific'97, Canberra, Springer Series in Discrete Mathematics and Theoretical Computer Science, Springer, 1998, pp. 61-80, ISBN 981-4021-16-4.
The Refinement Calculator: Proof Support for Program Refinement. M.J. Butler, J. Grundy, T. Långbacka, R. Ruksenas, and J. von Wright. In L. Groves and S. Reeves, (Eds.), Formal Methods Pacific'97, Wellington, New Zealand, Springer Series in Mathematics and Theoretical Computer Science. Springer, 1997, pp. 40-61, ISBN 981-3083-31-X.
An Approach to the Design of Distributed Systems with B AMN. M.J. Butler. In J. Bowen, M. Hinchey, D. Till (Eds.) 10th International Conference of Z Users (ZUM'97), 3-4th April 1997, Reading, UK, LNCS 1212, Springer-Verlag, 1997, pp. 223-241, ISBN 3-540-62717-0.
Distributed System Development in B. M.J. Butler and M. Waldén. First B Conference, Nantes, France, November 25-28, 1996, pp. 155-168, ISBN 2-906082-25-2.
An Action System Approach to the Steam Boiler Problem. M. Butler, E. Sekerinski, K. Sere. In Formal Methods for Industrial Applications: Specifying and Programming the Steam Boiler Control, Jean-Raymond Abrial, Egon Börger and Hans Langmaack (Eds.), LNCS 1165, Springer-Verlag, 1996, pp. 129-148, ISBN 3-540-61929-1.
Program Derivation Using the Refinement Calculator. M.J. Butler and T. Långbacka. In J. von Wright, J. Grundy, J. Harrison (Eds.), TPHOLs'96, August 1996, Turku, Finland, LNCS 1125, Springer-Verlag, 1996, pp. 93-108, ISBN 3-540-61587-3.
Calculational Derivation of Algorithms on Tree-based Pointer Structures. M.J. Butler. In He Jifeng, J. Cooke and P. Wallis (Eds.), 7th BCS-FACS Refinement Workshop, Bath, UK, July 1996, ISBN 3-540-76104-7.
Exploring Summation and Product Operators in the Refinement Calculus. R.J.R. Back and M.J. Butler. In B. Möller (Ed.) Mathematics of Program Construction, Kloster Irsee, Germany, LNCS 947, Springer-Verlag July 1995.
Applications of Summation and Product Operators in the Refinement Calculus. R.J.R. Back and M.J. Butler. 6th Nordic Workshop on Programming Theory, Aarhus, Denmark, 1994.
Refinement and Decomposition of Value-Passing Action Systems. M.J. Butler. In E. Best (Ed.), CONCUR'93, Hildesheim, Germany, LNCS 715, Springer-Verlag, 1993.
Behavioural Extension for CSP Processes. M.J. Butler. In S. Prehn and W.J. Toetenel (Eds.), VDM '91, Noordwijkerhout, The Netherlands, LNCS 551, Springer-Verlag, 1991.
Service Extension at the Specification Level. M.J. Butler. In J.E. Nicholls (Ed.), Z User Meeting, Oxford, UK, 1990.

Other

Towards a UML profile for UML-B. Snook, C., Butler, M. and Oliver, I., Technical Report DSSE-TR-2003-3, Electronics and Computer Science, University of Southampton.
Contracts for Scenario-Based Testing of Object-Oriented Programs. Mikhailova, A., Doche, M. and Butler, M. (2002).
Refinement of Dynamic Systems. Stefan Hallerstede and Michael Butler. University of Southampton Declarative Systems & Software Engineering Technical Reports, DSSE-TR-99-8.
Using Refinement to Analyse the Safety of an Authentication Protocol. Michael Butler. University of Southampton Declarative Systems & Software Engineering Technical Reports, DSSE-TR-98-8.
Applying Formal Methods to the Design of Smart Card Software. Michael Butler, Pieter Hartel, Eduard de Jong and Mark Longley. University of Southampton Declarative Systems & Software Engineering Technical Reports, DSSE-TR-97-8.
Specification of a Program Derivation Editor. M.J. Butler, E. Hedman, P. Nilson, R. Ruksenas, M. WaldÈn, Y. Zhao. Åbo Akademi University reports in Mathematics and Computer Science, A94-157, 1994.
Formal Techniques Applied to the X.400 Reliable Transfer Service. M.J. Butler. M.Sc. Thesis, Programming Research Group, Oxford University, 1989.
Feature Interaction Analysis Using Z. M.J. Butler, Broadcom, Dublin. Thesis
A CSP Approach to Action Systems. M.J. Butler. D.Phil. thesis, Programming Research Group, Oxford University, 1992.

Updated 4 August 2004