Publications

Results 1–25 of 64
Skip to search filters

Formal verification of run-to-completion style statecharts using event-b

Communications in Computer and Information Science

Morris Wright, Karla V.; Snook, Colin; Hoang, Thai S.; Hulette, Geoffrey C.; Armstrong, Robert C.; Butler, Michael

Although popular in industry, state-chart notations with ‘run to completion’ semantics lack formal refinement and rigorous verification methods. State-chart models are typically used to design complex control systems that respond to environmental triggers with a sequential process. The model is usually constructed at a concrete level and verified and validated using animation techniques relying on human judgement. Event-B, on the other hand, is based on refinement from an initial abstraction and is designed to make formal verification by automatic theorem provers feasible. We introduce a notion of refinement into a ‘run to completion’ statechart modelling notation, and leverage Event-B ’s tool support for theorem proving. We describe the difficulties in translating ‘run to completion’ semantics into Event-B refinements and suggest a solution. We illustrate our approach and show how critical (e.g. safety) invariant properties can be verified by proof despite the reactive nature of the system. We also show how behavioural aspects of the system can be verified by testing the expected reactions using a temporal logic model checking approach.

More Details
TYPE Conference Poster YEAR 2020
ScopusOSTI

Refinement and Verification of Responsive Control Systems

Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

Morris Wright, Karla V.; Snook, Colin; Hoang, Thai S.; Hulette, Geoffrey C.; Armstrong, Robert C.; Butler, Michael

Statechart notations with ‘run to completion’ semantics, are popular with engineers for designing controllers that respond to events in the environment with a sequence of state transitions. However, they lack formal refinement and rigorous verification methods., on the other hand, is based on refinement from an initial abstraction and is designed to make formal verification by automatic theorem provers feasible. We introduce a notion of refinement into a ‘run to completion’ statechart modelling notation, and leveragetool support for theorem proving. We describe the difficulties in translating ‘run to completion’ semantics intorefinements and suggest a solution. We outline how safety and liveness properties could be verified.

More Details
TYPE Conference Poster YEAR 2020
ScopusOSTIDOI

A Mesh-Free Method to Predictively Simulate Solid-to-Liquid Phase Transitions in Abnormal Thermal Environments

Templeton, Jeremy A.; Erickson, Lindsay C.; Morris Wright, Karla V.

Particle methods in computational physics are useful for modeling the motion of fluids and solids subject to large deformations. Under these conditions, mesh-based approaches often fail due to decreasing element quality leading to inaccuracy and instability. The developed software package called Moab investigates and prototypes next-generation particle methods, focusing on rigorous error analysis and active error minimization strategies during the computation. The present work discusses examples calculations representative of real engineering problems with quantified and maximized accuracy while demonstrating the potential for meeting engineering performance re- quirements.

More Details
TYPE SAND Report YEAR 2016
OSTIDOI
Results 1–25 of 64
Results 1–25 of 64