Title :
Animated, user friendly, formal specifications
Author :
Warren, John H. ; Pynn, Cathy ; Oldman, Robin D.
Author_Institution :
Precision Design Technol. Ltd., Maidenhead, UK
Abstract :
Discusses PRECIS, a method for specifying sequential, non-concurrent systems based on a first order predicate logic. It operates by use of entities and the use of relationships between these entities. Since the method has a mathematical foundation, it is possible to reason logically about the properties of system specifications. It is also possible to test hypotheses and to attempt proofs to validate these hypotheses. The PRECIS method has a mathematical foundation and thus offers the possibilities of reasoning logically about the properties of specifications and proving theorems about the system being specified. Hence it satisfies the needs of safety critical systems in particular by allowing hypotheses to be put forward and tested
Keywords :
formal logic; formal specification; inference mechanisms; PRECIS method; entity relationship; first order predicate logic; formal specifications; non-concurrent systems; reasoning; sequential systems;
Conference_Titel :
Automating Formal Methods for Computer Assisted Prototying, IEE Colloquium on
Conference_Location :
London
