Query Generation Guidelines for Statecharts WITHIN Object-Oriented Designs

H. Liu and D.P. Gluch (USA)


: Software Engineering, Model Check, LinearTemporal Logic, ObjectProcess Methodology.


This paper provides preliminary results in defining guidelines for generating Linear Temporal Logic (LTL) queries for model checking Statecharts within an object oriented design and in establishing a framework for eliciting informal queries from requirements documents. Since formal queries are verified against a design element, a semantic gap exists between requirement properties and formal queries. This gap can present a serious challenge in expressing informal queries that are easily translated into formal ones. However, if within object-oriented designs, an object-process methodology is used to guide Statechart modeling, the semantic gap can be bridged and proper informal queries can be readily elicited.

Important Links:

Go Back