Title :
A case study of using SOFL to specify a concurrent software system
Author_Institution :
Sch. of Electron., Inf., & Electr. Eng., Shanghai Jiao Tong Univ., Shanghai, China
Abstract :
SOFL, a formal engineering method which was designed by integrating different notations and techniques, can be used for specification and verification of large-scale software systems. Regions and channels can also be introduced to the SOFL language so that concurrency can be easily specified in the specification of a concurrent software system. In this paper we present a case study of using SOFL specification language for specifying a concurrent software system in order to show the usability of regions and channels in modeling. We also discuss some important issues about the specifications of concurrent software systems.
Keywords :
concurrency control; formal specification; formal verification; SOFL specification language; concurrent software system; formal engineering method; large-scale software system verification; Concurrent computing; Message passing; Software systems; Specification languages; System recovery; Usability; Concurrent software; SOFL specification language; case study;
Conference_Titel :
Software Engineering and Service Sciences (ICSESS), 2010 IEEE International Conference on
Conference_Location :
Beijing
Print_ISBN :
978-1-4244-6054-0
DOI :
10.1109/ICSESS.2010.5552303
