Abstract
SOFL is a well-known industrially applied software design language to be used within the framework of a formal engineering method (FEM). Though SOFL is easy to grasp and intuitively usable by practitioners, its original syntax permits the construction of ‘funny’ specifications (which cannot sensibly be implemented) and its semantics is not precisely defined. In the project described in this paper we have defined a restricted dialect of SOFL which can be parsed for syntactical correctness, and the semantics of which is well-defined. The static semantics of a SOFL specification can now be formally checked by means of an SMT solver, (SMT: Satisfiability ‘modulo theory’) whereas the dynamic semantics is provided by way of translation into a process algebra (the semantics of which is already given). Already available process algebra tools can then be used to formally check a well-constructed SOFL specification for interesting behavioural properties.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
EMF: Eclipse Modeling Framework.
- 2.
For the definition of ‘satisfiability’ in SOFL see [14, Definition 25, p. 304].
- 3.
In earlier work we demonstrated the usefulness of such a ‘translational’ approach in the context of CSP specifications of wireless sensor networks [25].
- 4.
Working with approximations is very common in the field of formal methods.
- 5.
- 6.
As we are addressing our paper to an audience of SOFL experts, we presume throughout this paper that our readers are already familiar with the contents of [14].
- 7.
Personal communication (e-mail) by Shaoying Liu: “In principle, SOFL specification inspection does not support formal proof simply because it is rather difficult for ordinary engineers, but for some critical applications formal proof may be valuable” (8 Nov. 2013).
- 8.
- 9.
This had been noticed by one of our anonymous reviewers.
- 10.
This, too, had been noticed by one of our anonymous reviewers.
- 11.
One of our anonymous reviewers has made such a remark. The list operators used in the example of above can be found in [14, Sect. 9.3].
- 12.
The relevant assertions on this topic can be found ‘scattered’ across [14, Rule 5.1, Rule 5.2, Definition 14, Definition 17, Definition 27, Definition 30 in Chap. 5 and Chap. 17].
- 13.
For comparison see the concept of ‘Value-Space-based Sub-Typing’ [22].
- 14.
During the historic evolution of SOFL, those object-oriented features were simply ‘plugged onto’ the already existing older functional features, thus ‘cluttering’ the entire language with much redundancy.
- 15.
One of our anonymous reviewers had made a comment on this point.
- 16.
Strictly speaking we have thus an ‘SFL’ dialect without the Object-oriented ‘O’.
- 17.
Shortage of page-space in this paper does not allow us to illustrate the very dense description of above with a picture; the full explanation will appear in [2].
- 18.
One of our anonymous reviewers had made such a remark.
- 19.
- 20.
Intel i7-6700 CPU.
- 21.
‘Processes’ in SOFL may be considered as ‘functions plus side-effects’, in contrast to the ‘pure’ functions that SOFL also allows to be specified [14, Sect. 4.17].
References
Barrett, C., Fontaine, P., Tinelli, C.: The SMT-LIB Standard: Version 2.6. Technical report, University of Iowa (2017). www.SMT-LIB.org
van der Berg, J.S.: A New Dialect of SOFL: Syntax, Formal Semantics, and Tool Support. M.-Thesis, University of Pretoria (forthcoming)
Bergstra, J., Klop, J.: Process algebra for synchronous communication. Inf. Control 60, 109–137 (1984)
Blom, S., van de Pol, J., Weber, M.: LTSmin: distributed and symbolic reachability. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 354–359. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-14295-6_31
Bruce, K.B.: Foundations of Object-Oriented Languages: Types and Semantics. MIT Press, Cambridge (2002)
Chen, Y.: Checking internal consistency of SOFL specification: a hybrid approach. In: Liu, S., Duan, Z. (eds.) SOFL+MSVL 2013. LNCS, vol. 8332, pp. 175–191. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-04915-1_13
Dong, J.S., Liu, S.: An object semantic model of SOFL. In: Araki, K., Galloway, A., Taguchi, K. (eds.) IFM’99, pp. 189–208. Springer, London (1999). https://doi.org/10.1007/978-1-4471-0851-1_11
Ho-Stuart, C., Liu, S.: A formal operational semantics for SOFL. In: Joint Proceedings of the 4th International Computer Science Conference and 4th Asia Pacific Software Engineering Conference, pp. 52–61. IEEE (1997)
Li, M., Liu, S.: Automated functional scenarios-based formal specification animation. In: Proceedings of the 19th Asia-Pacific Software Engineering Conference, pp. 107–115. IEEE (2012)
Li, M., Liu, S.: Tool support for rigorous formal specification inspection. In: Proceedings of the 17th International Conference on Computational Science and Engineering, pp. 729–734. IEEE (2014)
Li, C., Liu, S., Nakajima, S.: An experiment for assessment of a functional scenario-based test case generation method. In: Proceedings of International Conference on Software Engineering and Technology, ICSET 2012, pp. 424–431 (2012)
Liu, S.: A Case Study of Modeling an ATM Using SOFL. Technical report, Hosei University (2003)
Liu, S.: A rigorous approach to reviewing formal specifications. In: Proceedings of 27th Annual NASA Goddard IEEE Software Engineering Workshop, pp. 75–81. IEEE (2002/2003)
Liu, S.: Formal engineering for industrial software development – an introduction to the SOFL specification language and method. In: Davies, J., Schulte, W., Barnett, M. (eds.) ICFEM 2004. LNCS, vol. 3308, pp. 7–8. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-30482-1_4
Liu, S.: Utilizing specification testing in review task trees for rigorous review of formal specifications. In: Proceedings of the 10th Asia-Pacific Software Engineering Conference, pp. 510–519. IEEE (2003)
Liu, S., Asuka, M., Komaya, K., Nakamura, Y.: Applying SOFL to specify a railway crossing controller for industry. In: Proceedings of the 2nd IEEE Workshop on Industrial Strength Formal Specification Techniques, pp. 16–27 (1998)
Liu, S., Shibata, M., Sato, R.: Applying SOFL to develop a university information system. In: Proceedings of the 6th Asia-Pacific Software Engineering Conference, pp. 404–411. IEEE (1999)
Liu, S., Sun, Y.: Structured methodology \(+\) object-oriented methodology \(+\) formal methods: methodology of SOFL. In: Proceedings of the 1st IEEE International Conference on Engineering of Complex Computer Systems, ICECCS 1995, pp. 137–144. IEEE (1995)
Liu, S., Wang, H.: An automated approach to specification animation for validation. J. Syst. Softw. 80(8), 1271–1285 (2007)
Liu, S., Woodcock, J.: Supporting rigorous reviews of formal specifications using fault trees. In: Proceedings of 16th World Computer Congress Conference on Software: Theory and Practice, pp. 459–470 (2000)
de Moura, L., Bjørner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-78800-3_24
Paar, A., Gruner, S.: Static typing with value-space-based subtyping. In: Proceedings of the South African Institute of Computer Scientists and Information Technologists, SAICSIT 2011, pp. 177–186. ACM (2011)
Sewell, P., et al.: Ott: effective tool support for the working semanticist. J. Funct. Program. 20(1), 71–122 (2010)
Stappers, F.P.M., Reniers, M.A., Groote, J.F.: Suitability of mCRL2 for concurrent-system design: a \(2 \times 2\) switch case study. In: de Boer, F.S., Bonsangue, M.M., Hallerstede, S., Leuschel, M. (eds.) FMCO 2009. LNCS, vol. 6286, pp. 166–185. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-17071-3_9
Steyn, T.J., Gruner, S.: A new optional parallelism operator in CSP for wireless sensor networks. In: Proceedings of the South African Institute of Computer Scientists and Information Technologists, SAICSIT 2017, pp. 303–310. ACM (2017)
Tian, C., Liu, S., Duan, Z.: Abstract model checking with SOFL hierarchy. In: [16], pp. 71–86 (2013)
Wadler, P.: Propositions as types. Commun. ACM 58(12), 75–84 (2015)
Wang, J., Liu, S., Qi, Y., Hou, D.: Developing an insulin pump system using the SOFL method. In: Proceedings of the 14th Asia-Pacific Software Engineering Conference, pp. 334–341. IEEE (2007)
Wang, X., Liu, S.: Development of a supporting tool for formalizing software requirements. In: Liu, S. (ed.) SOFL 2012. LNCS, vol. 7787, pp. 56–70. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-39277-1_5
Zainuddin, F.B., Liu, S.: An approach to low-fidelity prototyping based on SOFL informal specification. In: 19th Asia-Pacific Software Engineering Conference, pp. 654–663. IEEE (2012)
Acknowledgements
During the course of our project several discussions with the following experts were especially helpful: Shaoying Liu, Markus Roggenbach, Jan Friso Groote, Stefan Blom, Jaco v.d. Pol, and Christian Dietrich. We thank the anonymous reviewers for their insightful comments on our paper’s draft before the SOFL\(+\)MSVL‘18 workshop, and we also acknowledge the interesting discussion contributions by various participants of the workshop following our paper’s presentation in Australia.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2019 Springer Nature Switzerland AG
About this paper
Cite this paper
van der Berg, J., Gruner, S. (2019). Formal Semantics and Tool Support for a Syntactically Restricted Dialect of SOFL. In: Duan, Z., Liu, S., Tian, C., Nagoya, F. (eds) Structured Object-Oriented Formal Language and Method. SOFL+MSVL 2018. Lecture Notes in Computer Science(), vol 11392. Springer, Cham. https://doi.org/10.1007/978-3-030-13651-2_8
Download citation
DOI: https://doi.org/10.1007/978-3-030-13651-2_8
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-13650-5
Online ISBN: 978-3-030-13651-2
eBook Packages: Computer ScienceComputer Science (R0)