Access Restriction

Author Bultan, Tevfik
Source CiteSeerX
Content type Text
File Format PDF
Language English
Subject Domain (in DDC) Computer science, information & general works ♦ Data processing & computer science
Subject Keyword Challenging Goal ♦ Model Checker Generates ♦ Original Specification ♦ Introduction Developing Reliable Software ♦ Model Checking ♦ Keywords Reactive System ♦ Compositional Model ♦ Software Specification ♦ Information Technology ♦ Modular Specification ♦ Assembly Language ♦ Transition System Model ♦ Action Language ♦ Asynchronous System ♦ Action Language Translation ♦ Typical Example ♦ Scr Specification ♦ Model Checking Reactive System ♦ Reactive System ♦ Programming Language ♦ Specification Language ♦ High Level Specification Language
Description In Proceedings of the 22nd International Conference on Software Engineering (ICSE 2000
We present a specification language called Action Language for model checking software specifications. Action Language forms an interface between transition system models that a model checker generates and high level specification languages such as Statecharts, RSML and SCR---similar to an assembly language between a microprocessor and a programming language. We show that Action Language translations of Statecharts and SCR specifications are compact and they preserve the structure of the original specification. Action Language allows specification of both synchronous and asynchronous systems. It also supports modular specifications to enable compositional model checking. Keywords Reactive systems, specification languages, model checking. 1 INTRODUCTION Developing reliable software for reactive systems is one of the most challenging goals in information technology. A reactive system is one which interacts with its environment continuously without terminating [22]. Typical examples ar...
Educational Role Student ♦ Teacher
Age Range above 22 year
Educational Use Research
Education Level UG and PG ♦ Career/Technical Study
Learning Resource Type Article
Publisher Date 2000-01-01