%0 Thesis %1 bussow__model %A Büssow, Robert %D 2002 %K methods formal verification 2002 statecharts model_checking z thesis %T Model Checking Combined Z and Statechart Specifications %U http://edocs.tu-berlin.de/diss/2003/buessow_robert.htm %X One of today's major problems in software engineering is to achieve a high and comprehensive quality standard for the software development process, in order to maintain a reliable high quality for the resulting products. This holds particularly true for safety critical systems, where failure of the software may have life-threatening consequences. Here, not only the quality of the software itself is important, but also the ability to convince a third party of this very quality. The usage of formal methods is one promising approach to achieve these goals. Roughly speaking, formal methods introduce mathematical precision to the development process. They do so by using formalisms with well defined semantics, and so stipulate formal proofs to verify development steps. This approach is all too well feasible in theory. In practice, however, one will encounter various problems that impede a consequent usage of formal methods: The formal character of the proposed languages and the need to use them for every aspect of the described system makes them too bulky. The reason for this is that they often times concentrate more on the mathematical elegance of their underlying semantics than on comfortable and intuitive usage. The specification language mSZ tackles this problem. It combines Harel’s Statecharts with the formal specification language Z and offers very intuitive means to describe a system. As adequate tool support is often missing, implementation of the formal proof obligations becomes practically impossible, because without any tools, these proofs are quite complicated, and their development takes a lot of time. Providing tool support for the verification of consistency and properties of an mSZ specification is the objective of this work. Model checking is used for the verification. An mSZ specification is translated in three steps into the input language of a model checker: The Statecharts are translated to Z. With this, the Statechart semantics and the semantics of the Statechart integration with Z are defined. The result of this translation can also be used by Z tools that do not know Statecharts for analysis. The Z specification is rewritten to a Z subset (Simple Z) that contains only language constructs, supported by the model checker. This step allows preparing mSZ as well as pure Z specifications for model checking. Simple Z is translated to the input language of the SMV model checker.

@phdthesis{bussow__model, abstract = {One of today's major problems in software engineering is to achieve a high and comprehensive quality standard for the software development process, in order to maintain a reliable high quality for the resulting products. This holds particularly true for safety critical systems, where failure of the software may have life-threatening consequences. Here, not only the quality of the software itself is important, but also the ability to convince a third party of this very quality. The usage of formal methods is one promising approach to achieve these goals. Roughly speaking, formal methods introduce mathematical precision to the development process. They do so by using formalisms with well defined semantics, and so stipulate formal proofs to verify development steps. This approach is all too well feasible in theory. In practice, however, one will encounter various problems that impede a consequent usage of formal methods: The formal character of the proposed languages and the need to use them for every aspect of the described system makes them too bulky. The reason for this is that they often times concentrate more on the mathematical elegance of their underlying semantics than on comfortable and intuitive usage. The specification language mSZ tackles this problem. It combines Harel’s Statecharts with the formal specification language Z and offers very intuitive means to describe a system. As adequate tool support is often missing, implementation of the formal proof obligations becomes practically impossible, because without any tools, these proofs are quite complicated, and their development takes a lot of time. Providing tool support for the verification of consistency and properties of an mSZ specification is the objective of this work. Model checking is used for the verification. An mSZ specification is translated in three steps into the input language of a model checker: The Statecharts are translated to Z. With this, the Statechart semantics and the semantics of the Statechart integration with Z are defined. The result of this translation can also be used by Z tools that do not know Statecharts for analysis. The Z specification is rewritten to a Z subset (Simple Z) that contains only language constructs, supported by the model checker. This step allows preparing mSZ as well as pure Z specifications for model checking. Simple Z is translated to the input language of the SMV model checker.}, added-at = {2009-02-12T11:53:09.000+0100}, author = {B"{u}ssow, Robert}, biburl = {https://www.bibsonomy.org/bibtex/2f7ac733241adb6153f5049a3647b8925/leonardo}, citeulike-article-id = {3508648}, interhash = {7c0825d44bc9a71563da9396e8284182}, intrahash = {f7ac733241adb6153f5049a3647b8925}, keywords = {methods formal verification 2002 statecharts model_checking z thesis}, posted-at = {2008-11-13 13:51:05}, priority = {2}, timestamp = {2009-02-12T11:53:09.000+0100}, title = {Model Checking Combined Z and Statechart Specifications}, url = {http://edocs.tu-berlin.de/diss/2003/buessow_robert.htm}, year = 2002 }