Event-based Models and Integrated Formal Methods
The historical development of formal methods saw a division between state based methods, with notations such as Z and B for developing sequential processes, and process algebra approaches whose main focus is to describe the communication patterns between such processes (CCS, CSP...). This has led us to consider the integration of formal methods, and the application of one formalism in the domain of another. The concept of a guarded event is a major tool in modelling distributed systems using a state based approach, and our papers contain many examples of event based models, including distributed booking systems, railway signalling models and interrupt driven schedulers. There is also some more theoretical work here which considers the relationship of refinement theories across different domains, requiring the introduction of backward refinement to complete the refinement scenario for the state based approach.
- S. E. Dunne and S. Conroy. Process refinement in B. In H. Treharne, S. King, M. C. Henson, and S. Schneider, editors, ZB2005: Formal Specification and Development in Z and B, number 3455 in Lecture Notes in Computer Science, pages 45-64. Springer, 2005.
- R. Hodgson and S. E. Dunne. Process, data and behaviour (perspectives on system development). Information and Software Technology, 32:539-544, 1990.