The paper proposes DDPSL (Drag and Drop PSL) a template library and a tool which simplifies the definition of PSL (Property Specification Language) formal properties by exploiting PSL-based templates. DDPSL allows users not expert in formal methods to define PSL properties by dragging and dropping logical and temporal operators, and variables from the design under verification (DUV) into predefined templates. Moreover, confident users or experts can extend the set of templates, reducing the effort required for formalizing complex properties. From the methodological point of view, DDPSL combines the advantages of both Open Verification Library (OVL) and PSL. Note that the templates are characterized by a parametric interface that separates the formal definition from its semantics, as provided by OVL. Moreover, the adoption of PSL as reference language guarantees the expressiveness of popular temporal logics such as Linear Temporal Logic (LTL) and Computational Tree Logic (CTL), which, on the contrary, are not fully supported by OVL. DDPSL has been successfully used to define properties for verifying an embedded application running on the microcontroller of an industrial oven.
DDPSL: an Easy Way of Defining Properties
DI GUGLIELMO, Luigi;FUMMI, Franco;ORLANDI, Nicola;PRAVADELLI, Graziano
2010-01-01
Abstract
The paper proposes DDPSL (Drag and Drop PSL) a template library and a tool which simplifies the definition of PSL (Property Specification Language) formal properties by exploiting PSL-based templates. DDPSL allows users not expert in formal methods to define PSL properties by dragging and dropping logical and temporal operators, and variables from the design under verification (DUV) into predefined templates. Moreover, confident users or experts can extend the set of templates, reducing the effort required for formalizing complex properties. From the methodological point of view, DDPSL combines the advantages of both Open Verification Library (OVL) and PSL. Note that the templates are characterized by a parametric interface that separates the formal definition from its semantics, as provided by OVL. Moreover, the adoption of PSL as reference language guarantees the expressiveness of popular temporal logics such as Linear Temporal Logic (LTL) and Computational Tree Logic (CTL), which, on the contrary, are not fully supported by OVL. DDPSL has been successfully used to define properties for verifying an embedded application running on the microcontroller of an industrial oven.
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
