Query Generation Guidelines for Statecharts WITHIN Object-Oriented Designs

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


: Software Engineering, Model Check, LinearTemporal Logic, Object-Process 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