Executable formal specifications of complex distributed systems with CoreASM

Formal specifications play a crucial role in the design of reliable complex software systems. Executable formal specifications allow the designer to attain early validation and verification of design using static analysis techniques and accurate simulation of the runtime behavior of the system-to-be...

Full description

Saved in:
Bibliographic Details
Published in:Science of computer programming 2014-01, Vol.79, p.23-38
Main Authors: Farahbod, Roozbeh, Gervasi, Vincenzo, Glässer, Uwe
Format: Article
Language:English
Subjects:
Abstract state machines
CoreASM
Extensible language
Formal methods
Specification and modeling environment
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:Formal specifications play a crucial role in the design of reliable complex software systems. Executable formal specifications allow the designer to attain early validation and verification of design using static analysis techniques and accurate simulation of the runtime behavior of the system-to-be. With increasing complexity of software-intensive computer-based systems and the challenges of validation and verification of abstract software models prior to coding, the need for interactive software tools supporting executable formal specifications is even more evident. In this paper, we discuss how CoreASM, an environment for writing and running executable specifications according to the ASM method, provides flexibility and manages the complexity by using an innovative extensible language architecture. ► We present CoreASM, a toolset for the design and analysis of high-level system models. ► The toolset supports authoring, running, and validation of formal specifications. ► Its novel extensible architecture allows extension of the language and interpreter. ►CoreASM has been deployed extensively in various scientific and industrial projects.
ISSN:0167-6423
1872-7964
DOI:10.1016/j.scico.2012.02.001