The following information was submitted:
Transactions: INTERNATIONAL JOURNAL of COMPUTERS
Transactions ID Number: 20-800
Full Name: Miroslav Popovic
Position: Professor
Age: ON
Sex: Male
Address: Faculty of Technical Sciences, Trg Dositeja Obradovica 6, 21000 Novi Sad, Serbia
Country: YUGOSLAVIA
Tel: 4801 101
Tel prefix: +381 21
Fax: 450 721
E-mail address: miroslav.popovic@rt-rk.com
Other E-mails:
Title of the Paper: Formal verification of embedded software based on software compliance properties and explicit use of time
Authors as they appear in the Paper: Miroslav Popovic and Ilija Basicevic
Email addresses of all the authors: miroslav.popovic@rt-rk.com,ilija.basicevic@rt-rk.com
Number of paper pages: 8
Abstract: The complexity of embedded software running in modern distributed large-scale systems is going so high that it becomes hardly manageable by humans. Formal methods and the supporting tools are offering effective means for mastering complexity, and therefore they are remaining to be an important subject of intensive research and development in both industry and academia. This paper makes a contribution to the overall R&D efforts in the area by proposing a method, and supporting tools, for formal verification of a class of embedded software, which may be modeled as a collection of distributed finite state machines. The method is based on the model checking of certain properties of embedded software models by Cadence SMV tool. These properties are systematically derived from the compliance test suites normally defined by relevant standards for compliance software testing, and therefore we refer to them as the compliance software properties. Another specificity of our a!
pproach is that we enable explicit usage of time within the software properties being verified, which gives more expressiveness to these properties and bring them more close to system properties that are analyzed in other engineering disciplines. The supporting tools enable generation of these models from the high-level design models and/or from the target source code, for example in C/C++ language. We demonstrate the usability of the proposed method on a case study. The subject of the case study is formal verification of distributed embedded software actually used in real telephone switches and call centers.
Keywords: Embedded software, Formal verification, Model checking, SDL language, SMV language
EXTENSION of the file: .doc
Special (Invited) Session: An Approach to Formal Verification of Embedded Software
Organizer of the Session: 659-115
How Did you learn about congress:
IP ADDRESS: 188.2.24.230
