Title :
Action Language: a specification language for model checking reactive systems
Author_Institution :
Dept. of Comput. Sci., California Univ., Santa Barbara, CA, USA
Abstract :
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 :
formal specification; specification languages; Action Language; RSML; SCR; SCR specifications; Statecharts; compositional model checking; microprocessor; model checking reactive systems; model checking software specifications; modular specifications; programming language; specification language; transition system models; Computer bugs; Embedded system; Hardware; Logic; Permission; Power system reliability; Software safety; Software systems; Specification languages; Thyristors;
Conference_Titel :
Software Engineering, 2000. Proceedings of the 2000 International Conference on
Conference_Location :
Limerick
Print_ISBN :
1-58113-206-9
DOI :
10.1109/ICSE.2000.870424