ADVANCE Publications

2014

• David Déharbe, Pascal Fontaine, Yoann Guyot, Laurent Voisin (2014) Integrating SMT solvers in Rodin. Sci. Comput. Program. 94: 130-143.
• Salehi Fathabadi, Asieh, Butler, Michael and Rezazadeh, Abdolbaghi (2014) Language and tool support of event refinement structures in Event-B. In, Formal Aspects of Computing (in press).
• Salehi Fathabadi, Asieh, Snook, Colin and Butler, Michael (2014) Applying an integrated modelling process to run-time management of many-core systems. In, 11th International Conference on Integrated Formal Methods (iFM), Bertinoro, IT, 09 - 11 Sep 2014.
• Savicks, Vitaly, Butler, Michael and Colley, John (2014) Co-Simulating Event-B and Continuous Models via FMI. In, 2014 Summer Computer Simulation Conference.
• Laurent Voisin, Jean-Raymond Abrial (2014) The Rodin Platform Has Turned Ten. In Proceedings ABZ'14, LNCS 8477, 2014.
• Dominik Hansen, Michael Leuschel (2014) Translating B to TLA + for Validation with TLC. In Proceedings ABZ'14, LNCS 8477, 2014.
• Michael Leuschel, David Schneider (2014) Towards B as a High-Level Constraint Modelling Language. In Proceedings ABZ'14, LNCS 8477, 2014.
• Andy Edmunds (2014) Templates for Event-B Code Generation. In Proceedings ABZ'14, LNCS 8477, 2014.
• Pereverzeva, Inna, Butler, Michael and Salehi Fathabadi, Asieh,  Laibinis, Linas and Troubitsyna, Elena. (2014) Formal Derivation of Distributed MapReduce. In Proceedings ABZ'14, LNCS 8477, 2014.
• Savicks, Vitaly, Butler, Michael and Colley, John (2014) Co-simulation Environment for Rodin: Landing Gear Case Study. In, In ABZ 2014: The Landing Gear Case Study, Springer Communications in Computer and Information Science, Vol. 433, 2014.
• Dominik Hansen, Lukas Ladenberger, Harald Wiegard, Jens Bendisposto, Michael Leuschel (2014) Validation of the ABZ Landing Gear System using ProB. In ABZ 2014: The Landing Gear Case Study, Springer Communications in Computer and Information Science, Vol. 433, 2014.
• Minh-Thang Khuu, Laurent Voisin, Fernando Mejia (2014) Modeling a Safe Interlocking Using the Event-B Theory Plug-in. In 5th Rodin User and Developer Workshop.
• Brett Bicknell, Karim Kanso, Jose Reis (2014) Smart Grids: Multi-Simulation, An Application. In 5th Rodin User and Developer Workshop.
• Asieh Salehi, Colin Snook, Michael Butler (2014) Run-time Management of Many-core Systems using Rodin. In 5th Rodin User and Developer Workshop.
• John Colley, Michael Butler (2014) From Untimed Specification to Cycle-Accurate Implementation - Cyber-Physical System Model Refinement with Event-B. In 5th Rodin User and Developer Workshop.
• Michael Leuschel, Jens Bendisposto and Dominik Hansen (2014) Unlocking the Mysteries of a Formal Model of an Interlocking System. In 5th Rodin User and Developer Workshop.
• Toby Wilkinson, Michael Butler, John Colley, Colin Snook  (2014) Generating Tests for COTS Components with Event-B and STPA. In 5th Rodin User and Developer Workshop.
• Colin Snook  (2014) iUML-B Statemachines. In 5th Rodin User and Developer Workshop.
• Daniel Plagge, Michael Leuschel (2014) A Practical Approach for Validation with Rodin Theories. In 5th Rodin User and Developer Workshop.
• Savicks, Vitaly, Butler, Michael, Colley, John and Bendisposto, Jens (2014) Rodin Multi-Simulation Plug-in. In, 5th Rodin User and Developer Workshop.
• Dominik Hansen, Jens Bendisposto, Michael Leuschel (2014) Integrating ProB into the TLA Toolbox. In TLA Workshop 2014.
• Sebastian Krings, Jens Bendisposto, Michael Leuschel (2014) Turning Failure into Proof: Evaluating the ProB Disprover. In Proceedings of the 1st International Workshop about Sets and Tools, 2014.
• Lukas Ladenberger, Ivaylo Dobrikov, Michael Leuschel (2014) An Approach for Creating Domain Specific Visualisations of CSP Models. In HOFM 2014, LNCS, 2014.
• Michael Leuschel, Jens Bendisposto, Ivaylo Dobrikov, Sebastian Krings, Daniel Plagge (2014) From Animation to Data Validation: The ProB Constraint Solver 10 Years On. In Jean-Louis Boulanger (ed.): Formal Methods Applied to Complex Systems: Implementation of the B Method, Wiley ISTE: 427-446, 2014.
• Jean-Charles Chaudemar, Vitaly Savicks, Michael Butler. (2014) Co-simulation of Event-B and Ptolemy II Models via FMI. In Embedded Real-time software and systems (ERTSS 2014).
• Bendisposto Jens, Krings Sebastian, Leuschel Michael (2014). Who watches the watchers: Validating the ProB Validation Tool. In Proceedings of the 1st Workshop on Formal-IDE, Electronic Proceedings in Theoretical Computer Science.
• Witulski John, Leuschel Michael (2014). Checking Computations of Formal Method Tools - A Secondary Toolchain for ProB. In Proceedings of the 1st Workshop on Formal-IDE, Electronic Proceedings in Theoretical Computer Science.

2013

• Hallerstede, Stefan, Jastram, Michael, Ladenberger, Lukas (2013). A Method and Tool for Tracing Requirements into Specifications. Science of Computer Programming.
• Hansen, Dominik, Leuschel, Michael (2013). Translating B to TLA+ for Validation with TLC: There and Back Again. Technical Report, No. STUPS/2013/xx, Institut für Informatik, Heinrich-Heine-Universität Düsseldorf, 2013.
• Krings, Sebastian Krings, Leuschel, Michael (2013). Inferring Physical Units in B Models. In Proceedings SEFM'2013, LNCS 8137, Springer, 2013.
• Clark, Joy (2013). Data Visualization in ProB. Bachelor Thesis.
• Zhang, Qinyuan (2013). Evaluierung des ProB Disprovers. Bachelor Thesis.
• Goebbels, René (2013). Worksheet für die Interaktion mit ProB. Bachelor Thesis.
• Kantner, Philipp (2013). Muster für die Verifikation von Formeln in Temporaler Logik. Master Thesis.
• Said, Mar Yah, Butler, Michael and Snook, Colin (2013). A Method of Refinement in UML-B. Software and Systems Modelling. To be published (accepted Nov 2013).
• Butler, Michael and Maamria, Issam (2013). Practical Theory Extension in Event-B. In, Festschrift Symposium in Honour of He Jifeng on the Occasion of His 70th Birthday.
• Dghaym, Dana, Butler, Michael and Salehi Fathabadi, Asieh (2013). Evaluation of graphical control flow management approaches for Event-B modelling. In, AVoCS 2013: 13th International Workshop on Automated Verification of Critical Systems, Guildford, UK.
• Banach, Richard and Butler, Michael (2013). A Hybrid Event-B Study of Lane Centering. In, Complex Systems Design & Management (CSD&M) 2013.
• Banach, Richard and Butler, Michael (2013). Cruise Control in Hybrid Event-B. In, International Colloquium on Theoretical Aspects of Computing (ICTAC), Shanghai 2013.
• Yeganefard, Sanaz and Butler, Michael (2013).  Problem Decomposition and Sub-Model Reconciliation of Control Systems in Event-B. In, IEEE International Workshop on Formal Methods Integration, 2013.
• Satpathy, M., Ramesh, S., Snook, Colin, Singh, N.K. and Butler, Michael (2013). A Mixed Approach to Rigorous Development of Control Designs. In, IEEE Multi-Conference on Systems and Control (MSC 2013).
• Vitaly Savicks, Michael Butler, Jens Bendisposto, John Colley (2013). Co-simulation of Event-B and Continuous Models in Rodin. In, 4th Rodin User and Developer Workshop. 
• Edmunds, Andrew (2013). Developments in Code Generation Tools for Event-B. In, 4th Rodin User and Developer Workshop. 
• Butler, Michael, Hallerstede, Stefan and Walden, Marina (eds.) (2013). Proceedings of the 4th Rodin User and Developer Workshop, TUCS (TUCS Publication Series).
• Colley, John and Butler, Michael (2013) A Formal, Systematic Approach to STPA using Event-B Refinement and Proof. In: 21th Safety Critical System Symposium, Bristol, UK.

2012

• Lecomte, Thierry, Burdy, Lilian, Leuschel, Michael (2012). Formally Checking Large Data Sets in the Railways. CoRR, abs/1210.6815, 2012.
• Butler, Michael (2012) Mastering System Analysis and Design through Abstraction and Refinement. Lectures at Marktoberdorf 2012 Summer School on Engineering Dependable Systems.
• Colley, John (2012) Tutorial: a Practical Introduction to using Event-B for Complex Hardware and Embedded System Specification and Design. Tutorial at FDL 2012, Vienna.
• Voisin, Laurent (2012) More Abstraction. In: AI meets Formal Software Development, 01-06.07.2012, Schloss Dagstuhl, Germany
• Edmunds, Andrew and Rezazadeh, Abdolbaghi and Butler, Michael (2012) Formal modelling for Ada implementations: Tasking Event-B. In: Ada-Europe 2012: 17th International Conference on Reliable Software Technologies, Stockholm.
• Edmunds, Andrew and Butler, Michael and Maamria, Issam and Silva, Renato and Lovell, Chris (2012) Event-B code generation: type extension with theories. In: ABZ 2012, 19-21 June 2012, Pisa, Italy.
• Jastram, Michael (2012) The ProR Approach: Traceability of Requirements and System Descriptions. PhD thesis, University of Dusseldorf.
• Plagge, Daniel and Leuschel, Michael (2012) Validating B, Z and TLA+ using ProB and Kodkod. In: Proceedings FM'2012, August, 2012, Paris.
• Weigelt, Ingo Architectures for an Extensible Text Editor for Rodin. Technical Report. University of Dusseldorf.
• Edmunds, Andrew and Colley, John and Butler, Michael Building on the DEPLOY legacy: code generation and simulation. In: DS-Event-B-2012: Workshop on the experience of and advances in developing dependable systems in Event-B.
• Renato Alexandre Silva: Lessons Learned/Sharing the Experience of Developing a Metro System Case Study. In: DS-Event-B-2012: Workshop on the experience of and advances in developing dependable systems in Event-B.