Cited By
View all- Luckcuck MFarrell MDennis LDixon CFisher M(2019)Formal Specification and Verification of Autonomous Robotic SystemsACM Computing Surveys10.1145/334235552:5(1-41)Online publication date: 13-Sep-2019
How to Select the Suitable Formal Method forźan Industrial Application: A Survey
Pages 213 - 228
Abstract
The share of formal methods is still marginal in contemporary systems and software engineering. One of the reasons is the absence of systematic guidelines and evaluation criteria that help software practitioners choose the right formal method for the problem at hand. In this paper, we present a comprehensive set of criteria, based on a systematic literature review and decade-long personal experience in industrial projects, for evaluating and comparing different formal methods. We argue that besides technical grounds e.g., modeling capabilities and supported development phases, formal methods should also be evaluated from social and industrial perspectives. At the end of the paper, we present an evaluation of "ABZ" methods based on the stipulated criteria.
References
[1]
Abdunabi, R., Sun, W., Ray, I.: Enforcing spatio-temporal access control in mobile applications. Computing 964, 313---353 2014
[2]
Abrial, J.R.: The B-Book: Assigning Programs to Meanings. Cambridge University Press, Cambridge 1996
[3]
Abrial, J.R.: Modeling in Event-B System and Software Design. Cambridge University Press, Cambridge 2010
[4]
Ardis, M.A., Chaves, J.A., Jagadeesan, L.J., Mataga, P., Puchol, C., Staskauskas, M.G., Von Olnhausen, J.: A framework for evaluating specification methods for reactive systems. IEEE Trans. Softw. Eng. 226, 378---389 1996
[5]
Banach, R.: Model based refinement and the tools of tomorrow. In: Börger, E., Butler, M., Bowen, J.P., Boca, P. eds. ABZ 2008. LNCS, vol. 5238, pp. 42---56. Springer, Heidelberg 2008
[6]
Banach, R., Zhu, H., Su, W., Huang, R.: Formalising the continuous/discrete modeling step. In: Proceedings Refine 2011. EPTCS, vol. 55, pp. 121---138 2011
[7]
Banach, R., Zhu, H., Su, W., Wu, X.: A continuous ASM modelling approach to pacemaker sensing. ACM Trans. Softw. Eng. Methodol. 241, 2 2014
[8]
Barjaktarovic, M.: The state-of-the-art in formal methods. Technical report/Wilkes University and WetStone Technologies 1998. http://www.cs.utexas.edu/users/csed/formal-methods/docs/StateFM.pdf
[9]
ter Beek, M.H., Bucchiarone, A., Gnesi, S.: Formal methods for service composition. Ann. Math. Comput. Teleinformatics 15, 1---10 2007
[10]
Börger, E., Stärk, R.: Abstract State Machines: A Method for High-Level System Design and Analysis. Springer, Berlin 2003
[11]
Boström, P., Degerlund, F., Sere, K., Waldén, M.: Derivation of concurrent programs by stepwise scheduling of Event-B models. Formal Aspects Comput. 262, 281---303 2014
[12]
Bowen, J.P.: Z: a formal specification notation. In: Frappier, M., Habrias, H. eds. Software Specification Methods: An Overview Using a Case Study, pp. 3---19. Springer, London 2001
[13]
Bowen, J.P., Hinchey, M.G.: Ten commandments of formal methods. Computer 284, 56---63 1995
[14]
Brunel, J., Rioux, L., Paul, S., Faucogney, A., Vallée, F.: Formal safety and security assessment of an avionic architecture with Alloy. In: Third International Workshop on Engineering Safety and Security Systems ESSS 2014, pp. 8---19 2014
[15]
Clarke, E.M., Wing, J.M.: Formal methods: state of the art and future directions. ACM Comput. Surv. 284, 626---643 1996
[16]
Cochran, D., Kiniry, J.R.: Formal model-based validation for tally systems. In: Heather, J., Schneider, S., Teague, V. eds. Vote-ID 2013. LNCS, vol. 7985, pp. 41---60. Springer, Heidelberg 2013
[17]
Cohen, E., Dahlweid, M., Hillebrand, M., Leinenbach, D., Moskal, M., Santen, T., Schulte, W., Tobies, S.: VCC: a practical system for verifying concurrent C. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. eds. TPHOLs 2009. LNCS, vol. 5674, pp. 23---42. Springer, Heidelberg 2009
[18]
Dondossola, G.: Formal methods in the development of safety critical knowledge-based components. In: Proceedings of the KR 1998 European Workshop on Validation and Verification of Knowledge-Based Systems, pp. 232---237 1998
[19]
Dwivedi, A.K., Rath, S.K.: Model to specify real time system using Z and Alloy languages: a comparative approach. In: International Conference on Software Engineering and Mobile Application Modelling and Development ICSEMA 2012, pp. 1---6 2012
[20]
Ferrarotti, F., Schewe, K., Tec, L., Wang, Q.: A new thesis concerning synchronised parallel computing - simplified parallel ASM thesis. CoRR abs/1504.06203 2015
[21]
Frappier, M., Habrias, H. eds.: Software Specification Methods. ISTE, London 2006
[22]
Frias, M.F., Pombo, C.G.L., Aguirre, N.M.: An equational calculus for alloy. In: Davies, J., Schulte, W., Barnett, M. eds. ICFEM 2004. LNCS, vol. 3308, pp. 162---175. Springer, Heidelberg 2004
[23]
Gannon, J.D., Zelkowitz, M.V., Purtilo, J.M.: Software Specification: A Comparison of Formal Methods. Greenwood Publishing, Westpoint 1994
[24]
Georg, G., Bieman, J., France, R.B.: Using Alloy and UML/OCL to specify run-time configuration management: a case study. In: Workshop of the pUML-Group Held Together with the UML 2001 on Practical UML-Based Rigorous Development Methods - Countering or Integrating the eXtremists, pp. 128---141, GI 2001
[25]
Ghezzi, C., Mandrioli, D., Morzenti, A.: TRIO: a logic language for executable specifications of real-time systems. J. Syst. Softw. 122, 107---123 1990
[26]
Haughton, H.P.: Using Z to model and analyse safety and liveness properties of communication protocols. Inf. Softw. Technol. 338, 575---580 1991
[27]
Hoang, T.S., Abrial, J.-R.: Event-B decomposition for parallel programs. In: Frappier, M., Glässer, U., Khurshid, S., Laleau, R., Reeves, S. eds. ABZ 2010. LNCS, vol. 5977, pp. 319---333. Springer, Heidelberg 2010
[28]
Holzmann, G.J.: The SPIN Model Checker: Primer and Reference Manual. Addison-Wesley, Reading 2004
[29]
Jackson, D.: Software Abstractions: Logic, Language, and Analysis. MIT Press, Cambridge 2006
[30]
Jones, C.B.: Systematic Software Development Using VDM, 2nd edn. Prentice-Hall Inc., Upper Saddle River 1990
[31]
Kang, E., Jackson, D.: Formal modeling and analysis of a flash filesystem in Alloy. In: Börger, E., Butler, M., Bowen, J.P., Boca, P. eds. ABZ 2008. LNCS, vol. 5238, pp. 294---308. Springer, Heidelberg 2008
[32]
Kaur, A., Gulati, S., Singh, S.: Analysis of three formal methods - Z, B and VDM. Int. J. Eng. Res. Technol. IJERT 14, 1---4 2012
[33]
Knight, J.C., DeJong, C.L., Gibble, M.S., Nakano, L.G.: Why are formal methods not used more widely? In: The Fourth NASA Langley Formal Methods Workshop LFM 1997 1997
[34]
Kossak, F.: Landing gear system: an ASM-based solution for the ABZ case study. In: Boniol, F., Wiels, V., Ait Ameur, Y., Schewe, K.-D. eds. ABZ 2014. CCIS, vol. 433, pp. 142---147. Springer, Heidelberg 2014
[35]
Kossak, F., Illibauer, C., Geist, V., Kubovy, J., Natschläger, C., Ziebermayr, T., Kopetzky, T., Freudenthaler, B., Schewe, K.D.: A Rigorous Semantics for BPMN 2.0 Process Diagrams. Springer, Heidelberg 2015
[36]
Kossak, F., Mashkoor, A.: How to Evaluate the Suitability of a Formal Method for Industrial Deployment? A Survey. Technical report SCCH-TR-1603, Software Competence Center Hagenberg GmbH, Hagenberg, Austria 2016. http://www.scch.at/en/rse-news/fm_comparison
[37]
Kossak, F., Mashkoor, A., Geist, V., Illibauer, C.: Improving the understandability of formal specifications: an experience report. In: Salinesi, C., van de Weerd, I. eds. REFSQ 2014. LNCS, vol. 8396, pp. 184---199. Springer, Heidelberg 2014
[38]
Lamport, L.: Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley, Boston 2002
[39]
Larsen, P.G., Wolff, S.: Development process of distributed embedded systems using VDM, Overture --- Open-source Tools for Formal Modelling TR-2010-02 2010
[40]
Liu, X., Yand, H., Zedan, H.: Formal methods for the re-engineering of computing systems. In: Proceedings of the 21st Computer Software and Applications Conference COMPSAC 1997, pp. 409---414 1997
[41]
Maoz, S., Ringert, J.O., Rumpe, B.: Semantically configurable consistency analysis for class and object diagrams. In: Whittle, J., Clark, T., Kühne, T. eds. MODELS 2011. LNCS, vol. 6981, pp. 153---167. Springer, Heidelberg 2011
[42]
Mashkoor, A., Biro, M.: Towards the trustworthy development of active medical devices: a hemodialysis case study. IEEE Embed. Syst. Lett. 81, 14---17 2016
[43]
Mashkoor, A., Hasan, O., Beer, W.: Using probabilistic analysis for the certification of machine control systems. In: Cuzzocrea, A., Kittl, C., Simos, D.E., Weippl, E., Xu, L. eds. CD-ARES Workshops 2013. LNCS, vol. 8128, pp. 305---320. Springer, Heidelberg 2013
[44]
Mashkoor, A., Jacquot, J.P.: Stepwise validation of formal specifications. In: 18th Asia-Pacific Software Engineering Conference APSEC 2011, pp. 57---64. IEEE, Ho Chi Minh City, Vietnam 2011
[45]
Mashkoor, A., Jacquot, J.P.: Utilizing Event-B for domain engineering: a critical analysis. Requirements Eng. 163, 191---207 2011
[46]
McGibbon, T.: An analysis of two formal methods: VDM and Z. Technical report, DoD Data and Analysis Center for Software DACS 1997. https://www.csiac.org/sites/default/files/An%20Analysis%20of%20Two%20Formal%20Methods%20-%20VDM%20and%20Z%20-%20SOAR.pdf
[47]
Merz, S.: The specification language TLA+. In: BjØrner, D., Henson, M. eds. Logics of Specification Languages. Monographs in Theoretical Computer Science, pp. 401---451. Springer, Heidelberg 2008
[48]
Mirian-HosseinAbadi, S.H., Mousavi, M.R.: Making nondeterminism explicit in Z. In: Proceedings of the Iranian Computer Society Annual Conference CSICC 2002, Tehran, Iran 2002
[49]
Mukherjee, P., Bousquet, F., Delabre, J., Paynter, S., Larsen, P.G.: Exploring timing properties using VDM++ on an industrial application. In: Proceedings of the Second VDM Workshop 2000
[50]
Newcombe, C.: Why Amazon chose TLA$$^+$$+. In: Ait Ameur, Y., Schewe, K.-D. eds. ABZ 2014. LNCS, vol. 8477, pp. 25---39. Springer, Heidelberg 2014
[51]
Newcombe, C., Rath, T., Zhang, F., Munteanu, B., Brooker, M., Deardeuff, M.: How amazon web services uses formal methods. Commun. ACM 584, 66---73 2015
[52]
Pandey, S., Batra, M.: Formal methods in requirements phase of SDLC. Int. J. Comput. Appl. 7013, 7---14 2013
[53]
Rainer-Harbach, M.: Methods and tools for the formal verification of software. An analysis and comparison. Diplomarbeit, Fakultät für Informatik, Technische Universität Wien. https://www.ads.tuwien.ac.at/publications/bib/pdf/rainer-harbach_11.pdf
[54]
Sifakis, J.: Formal methods and their evaluation. Position Paper Presented at FEMSYS in Munich 1997. http://www-verimag.imag.fr/~sifakis/RECH/FEMSYS/paper.ps
[55]
Spivey, J.M.: The Z Notation: A Reference Manual. Prentice-Hall Inc., Upper Saddle River 1989
[56]
Verhoef, M., Larsen, P.G., Hooman, J.: Modeling and validating distributed embedded real-time systems with VDM++. In: Misra, J., Nipkow, T., Sekerinski, E. eds. FM 2006. LNCS, vol. 4085, pp. 147---162. Springer, Heidelberg 2006
[57]
Wang, T., Ji, D.: Active attacking multicast key management protocol using Alloy. In: Derrick, J., Fitzgerald, J., Gnesi, S., Khurshid, S., Leuschel, M., Reeves, S., Riccobene, E. eds. ABZ 2012. LNCS, vol. 7316, pp. 164---177. Springer, Heidelberg 2012
[58]
Woodcock, J., Larsen, P.G., Bicarregui, J., Fitzgerald, J.: Formal methods: practice and experience. ACM Comput. Surv. 414, 19 2009
[59]
Zave, P.: A practical comparison of Alloy and Spin. Formal Aspects Comput. 20152, 239---253 2015
Recommendations
A new process algebra more suitable for formal specification
CSSE '21: Proceedings of the 4th International Conference on Computer Science and Software EngineeringThe paper shows that some usual specifications cannot be conveniently expressed in traditional process calculi. To solve the problem in formal specification, a new process calculus based on value-passing CCS, Calculus of Communicating Systems with ...
Formal Methods Application: An Empirical Tale of Software Development
The development of an elevator scheduling system by undergraduate students is presented. The development was performed by 20 teams of undergraduate students, divided into two groups. One group produced specifications by employing a formal method that ...
Towards a Formal Basis for the Formal Development Method and the Ina Jo Specification Language
Special issue on computer security and privacyIn carrying out SDC's Formal Development Method, one writes a specification of a system under design in the Ina Jo™ specification language and proves that the specification meets the requirements of the system. This paper develops an abstract machine ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
May 2016
415 pages
ISBN:9783319335995
Publisher
Springer-Verlag
Berlin, Heidelberg
Publication History
Published: 23 May 2016
Qualifiers
- Article
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- View Citations1Total Citations
- 0Total Downloads
- Downloads (Last 12 months)0
- Downloads (Last 6 weeks)0
Reflects downloads up to 20 Nov 2024
Other Metrics
Citations
Cited By
View all- Luckcuck MFarrell MDennis LDixon CFisher M(2019)Formal Specification and Verification of Autonomous Robotic SystemsACM Computing Surveys10.1145/334235552:5(1-41)Online publication date: 13-Sep-2019
View Options
View options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in