English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

Computer-Aided Software Engineering (CASE) tools encourage users to codify the requirements for the design of a system early in the development process. They often use graphical formalisms, simulation, and prototyping to help express ideas concisely and unambiguously. Some tools provide little more than syntax checking but others can test the model for reachability of conditions, nondeterminism, or deadlock. In this paper, we present an example of how commercial CASE tools can be linked with formal methods to build more thorough forms of analysis into these tools.The CASE tool STATEMATE [12] makes use of an extended state transition notation called statecharts. We have formalized the semantics of statecharts by embedding them in the logical framework of an interactive proof-assistant system called HOL. A software interface is provided to extract a statechart directly from the STATEMATE database and translate it into a textual representation that can be directly input into the HOL system.Using HOL in combination with Voss, a binary decision diagram-based verification tool, we have developed a model checker for statecharts, which tests whether an operational specification, given by a statechart, satisfies a descriptive specification of the system requirements. The model checking procedure is a simple higher-order logic function which executes the semantics of statecharts in Voss.This paper illustrates this method through two examples to show how our model checker may be used to aid in the analysis of the requirements of a system.

An example of linking formal methods with case tools: a model checker for statecharts