Towards a User-friendly Design and Verification Environment
this paper presents an environment for the verificationof complex concurrent software and hardware systems. Thetool is targeted at users who are not necessarily expert informal methods. The underlying mathematical specifica-tion language and verification methodologies are hidden tothe user by encapsulating them within a high-level environ-ment that supports graphical design, intuitive specificationof properties, high-leveldata representation, customised in-terfaces and pre-defined verification strategies. The seman-tic base of the tool is given by the Circal process algebra,which allows the internal representation of both the systemmodel and its properties within the same language.
In the last decades computers have been widely usedto control physical processes, mechanical devices, trans-portation and communication networks. As a result, thecomplexityofsoftwareandhardwarehasbeendramaticallyincreased, causing a non linear increase in human-error-induced design faults. Moreover, due to such software andhardware complexity, conventional testing methodologiesare nolongersufficient to guaranteecorrectness,safetyandsecurity of controlled computer systems. For these reasonsautomaticverificationofsoftwareandhardwareiscurrentlyone of the most important research topics in computer sci-ence and several formal methods tools [9] have been de-veloped aiming to provide automated or at least computer-aidedverification.The average user of design and verification tools is sel-dom an expert in formal methods and has more often anengineeringrather than mathematical background. For thisreason we need to encapsulateformal methodstools withina high-levelenviromentequippedwith user-friendlygraph-ical interfaces. Software andhardwaredevelopersare morefamiliarwith visualand tabularrepresentations,such as be-haviourtables,statediagrams,timingdiagrams,flowcharts,Petri nets [15] and statecharts [10]. However, such rep-resentations either provide a partial view of the system(behaviour tables, state diagrams, timing diagrams, flowcharts), or exist in several variants with many alternativesemantics (Petri nets), or even do not have a solid semanticbase (statecharts).Tools based on visual and tabular representations arevery limited and almost never have analytical features. Re-cently an attempt has been made in automatically verifyingproperties expressed in terms of timing diagrams [1], butonly a very small class of properties can be expressed inthis way. There are many Petri net-based tools and somestatecharts-based ones. However, Petri nets, even in theirmosthigh-leveldialects,areusuallysuitabletospecifyonlysome aspects of the system to be developed, at a specificabstraction level, but cannot in general cover all steps ofthe design. Statecharts can instead cover many aspects ofsyste mdesign, but the lack of a consolidatedse mantic basemakes it hard to give a mathematical interpretation to thevisual intuition.VS sewing machine
Inthispaper we aim to encapsulate previously developed methodologies[3, 4, 5, 6, 7, 8, 14] within a design and verificationenvironmentthatsupportsgraphicaldesign,thein-tegration of different formalisms and the intuitive specifi-cation of properties involving functional, timing and per-formance issues, and provides automatic tools for the ver-ification of these properties. By contrast to the statechartapproach,whereseveralattemptshavebeenmadetoretrofitsuitable semantics to the syntax [18], we want to build ourtool on the semantic base given by the Circal process alge-bra [14].Asthevisualcounterpartoftheprocessalgebraweadoptagraphicalrepresentationwhereaprocessisgivenbyabox(with communication ports on its outline) enclosing the fi-nitestate machinethatdefinesthe processbehaviour[8]. Incontrast to such a general representation, customised rep-resentations are defined to model some parts of the systemusing well-known formal methods, such as Petri nets, ordirectly model hardware systems at gate level or even atCMOS level.he paper presents a proposal of a user-friendly designand verification environment. Some of the interfaces andtechniques proposed have been already implemented usinggraphical interfaces [13, 16], some techniques exist just atthe processalgebralevel[5, 6, 7, 8, 14].In Section 2 we give the general architecture of the de-sign and verification environment. Section 3 describes thegraphical notation used by the tool and illustrates in detailthe software components of the environment that are de-voted to the design process. Section 4 describes analysistechniques for state-space exploration, simulation, testingandformal verification
Recent Comments