Title :
Towards a user-friendly design and verification environment
Author_Institution :
Software Verification Res. Centre, Queensland Univ., Qld., Australia
Abstract :
We present an environment for the verification of complex concurrent software and hardware systems. The tool is targeted at users who are not necessarily expert in formal methods. The underlying mathematical specification language and verification methodologies are hidden to the user by encapsulating them within a high-level environment that supports graphical design, intuitive specification of properties, high-level data representation, customised interfaces and predefined verification strategies. The semantic base of the tool is given by the Circal process algebra, which allows the internal representation of both the system model and its properties within the same language.
Keywords :
Petri nets; finite state machines; formal specification; formal verification; process algebra; specification languages; Circal process algebra; customised interfaces; formal methods; graphical design; hardware system verification; high-level data representation; mathematical specification language; semantic base; software system verification; user-friendly environment; Algebra; CMOS logic circuits; Communication system control; Design engineering; Hardware; Petri nets; Semiconductor device modeling; Software libraries; Software safety; Timing;
Conference_Titel :
Software Engineering Workshop, 2002. Proceedings. 27th Annual NASA Goddard/IEEE
Print_ISBN :
0-7695-1855-9
DOI :
10.1109/SEW.2002.1199478