SENov 27, 2018
Integrating User Design and Formal Models within PVSio-WebNathaniel Watson, Steve Reeves, Paolo Masci
Creating formal models of interactive systems has wide reaching benefits, not only for verifying low-level correctness, but also as a tool for ensuring user interfaces behave logically and consistently. Despite this, tools for designing user experiences and tools for creating and working with formal models are typically distinctly separate systems. This work aims to bridge this divide by allowing the generation of state machine diagrams and formal models via a simple, interactive prototyping tool that mirrors the basic functionality of many modern digital prototyping applications.
LOOct 20, 2018
Proceedings 18th Refinement WorkshopJohn Derrick, Brijesh Dongol, Steve Reeves
Refinement is one of the cornerstones of a formal approach to software engineering. Refinement is the process of developing a more detailed design or implementation from an abstract specification through a sequence of mathematically-based steps that maintain correctness with respect to the original specification. Work on the foundations of languages such as Z, B, VDM and CSP have led to their widespread use in certain industrial sectors, e.g., those with security or safety critical concerns. In addition to precise specification, formal methods also allow the possibility of precise and verifiable development, as captured by the concept of refinement. The 18th Refinement Workshop was held as part of FLoC 2018 at Oxford, UK.
SEMay 24, 2013
Proceedings 16th International Refinement WorkshopJohn Derrick, Eerke Boiten, Steve Reeves
The 16th BCS-FACS Refinement Workshop was co-located with iFM 2013 held in Turku, Finland on June 11th, 2013. This volume contains the 6 papers selected for presentation at the workshop following a peer review process. The papers cover a wide range of topics in the theory and application of refinement. Refinement is one of the cornerstones of a formal approach to software engineering: the process of developing a more detailed design or implementation from an abstract specification through a sequence of mathematically-based steps that maintain correctness with respect to the original specification.