Abstract
Formal specification animation is a very useful technique for verification and validation. It provides the end users and field experts with an intuitive way to observe the operational behaviour of software system described by the formal specification. Several tools have already been built to support animations of specifications written in different formal languages. In this paper, we describe the design of a tool that can support the animation of specification written in Structure Object-oriented Formal Language (SOFL). The animation strategy underlying the tool uses system functional scenario as a unit and data as connection among independent operations involved in one system functional scenario. A system functional scenario defines a behaviour that transforms input data into the output data through a sequential execution of operations. It is the target of animation. In the animation, data is used to connect each operation in a specific scenario. The data can be provided by the user or generated automatically. It will help the user and the developer to understand the system. We explain the whole animation process step by step and present a prototype at the end of the paper.
This work has been conducted as a part of “Research Initiative on Advanced Software Engineering in 2012” supported by Software Reliability Enhancement Center (SEC), Information Technology Promotion Agency Japan (IPA).
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
Combes, P., Dubois, F., Renard, B.: An open animation tool: application to telecommunication systems. Int. J. Comput. Telecommun. Netw. 40(5), 599–620 (2002)
Waeselynck, H., Behnia, S.: B model animation for external verification. In: Proceedings of the Second IEEE International Conference on Formal Engineering Methods, pp. 36–45 (1998)
Morrey, I., Siddiqi, J., Hibberd, R., Buckberry, G.: A toolset to support the construction and animation of formal specifications. J. Syst. Softw. 41(3), 147–160 (1998)
Liu, S.: Formal Engineering for Industrial Software Development Using the SOFL Method. Springer, Heidelberg (2004). ISBN 3-540-20602-7
Liu, S., Nakajima, S.: A Decompositional approach to automatic test case generation based on formal specification. In: Fourth IEEE International Conference on Secure Software Integration and Reliability Improvement, pp. 147–155 (2010)
Li, M., Liu, S.: Automated functional scenarios-based formal specification animation. In: Proceedings of the 19th Asia-Pacific Software Engineering Conference (APSEC 2012), pp. 107–115. IEEE CS Press, Hong Kong (2012)
Liu, S., Wang, H.: An automated approach to specification animation for validation. J. Syst. Softw. 80, 1271–1285 (2007)
Li, M., Liu, S.: Automatically generating functional scenarios from SOFL CDFD for specification inspection. In: 10th IASTED International Conference on Software Engineering, Innsbruck, Austria, pp. 18–25 (2011)
Stepien, B., Logrippo, L.: Graphic visualization and animation of LOTOS execution traces. Comput. Netw.: Int. J. Comput. Telecommun. Netw. 40(5), 665–681 (2002)
Liu, S., Chen, Y., Nagoya, F., McDermid, J.A.: Formal specification-based inspection for verification of programs. IEEE Trans. Softw. Eng. 21(2), 259–288 (2011). IEEE Computer Society Digital Library, IEEE Computer Society
Liu, S.: Integrating specification-based review and testing for detecting errors in programs. In: Butler, M., Hinchey, M.G., Larrondo-Petrie, M.M. (eds.) ICFEM 2007. LNCS, vol. 4789, pp. 136–150. Springer, Heidelberg (2007)
Miller, T., Strooper, P.: Model-based specification animation using testgraphs. In: George, C.W., Miao, H. (eds.) ICFEM 2002. LNCS, vol. 2495, pp. 192–203. Springer, Heidelberg (2002)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer International Publishing Switzerland
About this paper
Cite this paper
Li, M., Liu, S. (2014). SOFL Specification Animation with Tool Support. In: Liu, S., Duan, Z. (eds) Structured Object-Oriented Formal Language and Method. SOFL+MSVL 2013. Lecture Notes in Computer Science(), vol 8332. Springer, Cham. https://doi.org/10.1007/978-3-319-04915-1_9
Download citation
DOI: https://doi.org/10.1007/978-3-319-04915-1_9
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-04914-4
Online ISBN: 978-3-319-04915-1
eBook Packages: Computer ScienceComputer Science (R0)