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
