Title :
Arrays and contracts for the specification and analysis of regular systems
Author :
Maraninchi, Florence ; Morel, Lionel
Author_Institution :
VERIMAG, Gieres, France
Abstract :
We explore a structuring mechanism for reactive systems, based on two ideas: array iterators allow the description of regular systems; logical-time contracts allow local or global specifications of components. We describe a toolbox of automatic program manipulations able to exploit the regular structures and the contracts in order to help validating the system.
Keywords :
formal specification; parallel processing; program verification; array iterators; automatic program manipulations; global specifications; logical-time contracts; reactive systems; regular structures; regular systems; structuring mechanism; system validation; Contracts; Debugging; Design methodology; Equations; Formal verification; Large-scale systems; Logic arrays; Programmable logic arrays; Programming profession; System testing;
Conference_Titel :
Application of Concurrency to System Design, 2004. ACSD 2004. Proceedings. Fourth International Conference on
Print_ISBN :
0-7695-2077-4
DOI :
10.1109/CSD.2004.1309116
