Formal Specification as High-Level Programming: The ASSL Approach

作者: Emil Vassev , Mike Hinchey

DOI: 10.1007/978-1-4471-2350-7_9

关键词:

摘要: Formal methods aim to build correct software by eliminating both requirements and design flaws. Still, specification languages have a somewhat bad reputation in the engineering community for being too heavy difficult use. This is mainly due use of complex mathematical notations often requiring experts field. We rely on our experience show that writing formal specifications can be easier if language used as high-level programming language, where distinction between blurred. The Autonomic System Specification Language (ASSL) declarative autonomic systems with well-defined semantics. It implements modern concepts constructs such inheritance, modularity, type system, parameterization. Specifications written ASSL present view system under consideration, are intertwined.

参考文章(11)
Emil Vassev, Mike Hinchey, Software Verification of Autonomic Systems Developed with ASSL Foundations of Computer Software. Modeling, Development, and Verification of Adaptive Systems. pp. 1- 16 ,(2011) , 10.1007/978-3-642-21292-5_1
Donald E. Knuth, backus normal form vs. Backus Naur form Communications of the ACM. ,vol. 7, pp. 735- 736 ,(1964) , 10.1145/355588.365140
W. Truszkowski, M. Hinchey, J. Rash, C. Rouff, NASA's swarm missions: the challenge of building autonomous software IT Professional. ,vol. 6, pp. 47- 52 ,(2004) , 10.1109/MITP.2004.66
Emil Vassev, Mike Hinchey, ASSL Specification and Code Generation of Self-Healing Behavior for NASA Swarm-Based Systems 2009 Sixth IEEE Conference and Workshops on Engineering of Autonomic and Autonomous Systems. pp. 77- 86 ,(2009) , 10.1109/EASE.2009.12
Emil Vassev, Code Generation for Autonomic Systems with ASSL SERA (selected papers). pp. 69- 85 ,(2010) , 10.1007/978-3-642-13273-5_5
S.P. Miller, M. Srivas, Formal verification of the AAMP5 microprocessor: a case study in the industrial use of formal methods Proceedings of 1995 IEEE Workshop on Industrial-Strength Formal Specification Techniques. pp. 2- 16 ,(1995) , 10.1109/WIFT.1995.515475
IT Informatics, Backus-Naur Form Betascript Publishing. ,(2010)
Emil Iordanov Vassev, Joey Paquet, Towards a framework for specification and code generation of automatic systems Concordia University. ,(2008)
James Rumbaugh, Michael Blaha, Object-Oriented Modeling and Design with UML ,(1991)