Abstract
Formal specification languages are often criticized for being difficult to understand, difficult to use, and unacceptable by software practitioners. Notations based on state machines, such as, Statecharts, Requirements State Machine Language (RSML), and SCR, are suitable for modeling of embedded systems and eliminate many of the main drawbacks of formal specification languages. Although a specification language can help eliminate accidental complexity, the inherent complexity of many of today's systems inevitably leads to large and complex specifications. Thus, there is a need for mechanisms to simplify a formal specification and present information to analysts and reviewers in digestible chunks.
In this paper, we present a two tiered approach to slicing (or simplification) of hierarchical finite state machines. We allow an analyst to simplify a specification based on a scenario. The remaining behavior, called an interpretation of the specification, can then be sliced to extract the information effecting selected variables and transitions.
To evaluate the effectiveness and utility of slicing in hierarchical state machines, we have implemented a prototype tool and applied our slicing approach to parts of a specification of a large avionics system called TCAS II (Traffic alert and Collision Avoidance System II).
This work has been partially supported by NSF grants CCR-9624324 and CCR-9615088, and University of Minnesota Grant in Aid of Research 1003-521-5965.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
J. Chang and D.J. Richardson. Static and dynamic specification slicing. In Proceedings of the Fourth Irvine Software Symposium, April 1994.
D. Harel. Statecharts: A visual formalism for complex systems. Science of Computer Programming, 8:231–274, 1987.
D. Harel, H. Lachover, A. Naamad, A. Pnueli, M. Politi, R. Sherman, A. ShtullTrauring, and M. Trakhtenbrot. Statemate: A working environment for the development of complex reactive systems. IEEE Transactions on Software Engineering, 16(4):403–414, April 1990.
D. Harel and A. Naamad. The STATEMATE semantics of Statecharts. ACM Transactions on Software Engineering and Methodology, vol-5(4):293–333, October 1996.
D. Harel and A. Pnueli. On the development of reactive systems. In K.R. Apt, editor, Logics and Models of Concurrent Systems, pages 477–498. Springer-Verlag, 1985.
M. P.E. Heimdahl and N.G. Leveson. Completeness and Consistency Analysis of State-Based Requirements. In Proceedings of the 17th International Conference on Software Engineering, pages 3–14, April 1995.
M. P.E. Heimdahl and N.G. Leveson. Completeness and Consistency Analysis of State-Based Requirements. IEEE Transactions on Software Engineering, TSE22(6):363–377, June 1996.
C. L. Heitmeyer, R.D. Jeffords, and B. L. Labaw. Consistency checking of SCRstyle requirements specifications. ACM Transactions on Software Engineering and Methodology, vol-5(3):231–261, July 1996.
C. L. Heitmeyer, B. L. Labaw, and D. Kiskis. Consistency checking of SCR-style requirements specifications. In Proceedings of the International Symposium on Requirements Engineering, March 1995.
K. L. Heninger. Specifying software for complex systems: New techniques and their application. IEEE Transactions on Software Engineering, 6(1):2–13, January 1980.
D.J. Keenan and M.P.E. Heimdahl. Code generation from hierarchicl state machines. In Proceedings of the International Symposium on Requirements Engineering, 1997.
N. G. Leveson, M. P.E. Heimdahl, H. Hildreth, J. Reese, and R. Ortega. Experiences using Statecharts for a system requirements specification. In Proceedings of the Sixth International Workshop on Software Specification and Design, pages 31–41, 1991.
N. G. Leveson, M. P.E. Heimdahl, H. Hildreth, and J. D. Reese. Requirements specification for process-control systems. IEEE Transactions on Software Engineering, 20(9):694–707, September 1994.
T. Oda and K. Araki. Specification slicing in formal methods of software engineering. In Proceedings of the Seventeenth International Computer Software and Applications Conference, November 1993.
A.M. Sloane and J. Holdsworth. Beyond traditional program slicing. In Proceedings of the International Symposium on Software Testing and Analysis, pages 180–186, January 1996.
J.M. Spivy. The Z Notation: A Reference Manual. Prentice-Hall, 1992.
M. Weiser. Program slicing. IEEE Transactions on Software Engineering, SE-10(4):352–357, July 1984.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1997 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Heimdahl, M.P.E., Whalen, M.W. (1997). Reduction and slicing of hierarchical state machines. In: Jazayeri, M., Schauer, H. (eds) Software Engineering — ESEC/FSE'97. ESEC SIGSOFT FSE 1997 1997. Lecture Notes in Computer Science, vol 1301. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-63531-9_30
Download citation
DOI: https://doi.org/10.1007/3-540-63531-9_30
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-63531-4
Online ISBN: 978-3-540-69592-9
eBook Packages: Springer Book Archive