Now showing items 1-5 of 5
Compositional modelling: The formal perspective
We provide a formal framework within which an Information System (IS) could be modelled, analysed, and verified in a compositional manner. Our work is based on Interval Temporal Logic (ITL) and its programming language ...
A wide-spectrum language for object-based development of real-time systems.
(Elsevier Preprints, 1999-03-15)
A formal design notation is present whose underlying computational model is object-based. The object structure of the model is based on the practical, industry-strength Object Oriented structure development technique ...
Proving the correctness of the interlock mechanism in processor design.
(Chapman & Hall on behalf of the International Federation for Information Processing (IFIP), 1997)
In this paper, Interval Temporal Logic (ITL) us used to specify and verify the event processor EP/3, which is a multi-threaded pipeline processor capable of executing parallel programs. We first give the high level ...
ATOM: an object-based formal method for real-time systems
An object based formal method for the development of real-time systems, called ATOM, is presented. The method is an integration of the real-time formal technique TAM (Temporal Agent Model) with an industry-strength structured ...
Dynamic Access Control Policies - Specification and Verification
(Oxford University Press, 2012)
Security requirements deal with the protection of assets against unauthorized access (disclosure or modification) and their availability to authorized users. Temporal constraints of history-based access control policies ...