This site uses cookies to deliver our services and to ensure you get the best experience. By continuing to use this site, you consent to our use of cookies and acknowledge that you have read and understand our Privacy Policy, Cookie Policy, and Terms
Software systems are often model checked by translating them into a directly model-checkable formalism. Any serious software system requires application of compositional reasoning ...
This paper describes the lessons we learned over a thirteen year period while helping to develop the shutdown systems for the nuclear generating station at Darlington, Ontario, Can...
Safety is increasingly important for software based, critical systems. Fault tree analysis (FTA) is a safety technique from engineering, developed for analyzing and assessing syste...
We present a semantics for fault tree analysis, a technique used for the analysis of safety critical systems, in the real-time interval logic Duration Calculus with Liveness and sh...
As the systems we have to specify and verify become larger and more complex, there is a mounting need to combine different tools and decision procedures to accomplish large proof ...
Grigore Rosu, Steven Eker, Patrick Lincoln, Jos&ea...
: Real computer-based systems fail, and hence are often far less dependable than their owners and users need and desire. Individuals, organisations and indeed the world at large ar...
Abstract. UnifyingTheoriesofProgramming(UTP)canprovideaformalsemantic foundation not only for programming languages but also for more expressive specification languages. We believ...
Simple retrenchment is briefly reviewed in the B language of J.-R. Abrial [1] as a liberalisation of classical refinement, for the formal description of application developments ...
We present a novel application on model checking through SPIN as a means for verifying purely descriptive specifications written in TRIO, a first order, linear-time temporal logic ...
Angelo Morzenti, Matteo Pradella, Pierluigi San Pi...
Incomplete, inaccurate, ambiguous, and volatile requirements have plagued the software industry since its inception. The convergence of model-based development and formal methods o...
Steven P. Miller, Alan C. Tribble, Mats Per Erik H...