A novel type checker for software system specifications in RTPA

Author

Tan, Xinming ; Wang, Yingxu ; Ngolah, Cyprian F.

Author_Institution

Dept. of Electr. & Comput. Eng., Calgary Univ., Alta., Canada

Volume

3

fYear

2004

Firstpage

1549

Abstract

This paper presents a type checker for formal specifications of software systems described in real-time process algebra (RTPA). The grammar of RTPA is formally described by using the EBNF convention. Design and implementation techniques are presented that keep the RTPA syntax as close to its original mathematical notations as possible, and at the same time, allow it to be parsed easily as a super higher-level language. The tasks of type checking for RTPA specifications can be classified into three categories: (a) identifier type compliancy, (b) expression type compliancy, and (c) process constraint consistency. The RTPA type checker has been designed and implemented to support system architects and system analysts to ensure the correctness and consistency of system specifications to a maximum extent.

Keywords

computational linguistics; formal specification; grammars; process algebra; program compilers; program verification; EBNF convention; RTPA syntax; correctness; expression type compliancy; formal specifications; grammar; identifier type compliancy; process constraint consistency; real-time process algebra; software system specifications; super higher-level language; type checker; Acceleration; Algebra; Computer architecture; Drives; Formal specifications; Large-scale systems; Logic; Real time systems; Software engineering; Software systems;

fLanguage

English

Publisher

ieee

Conference_Titel

Electrical and Computer Engineering, 2004. Canadian Conference on

ISSN

0840-7789

Print_ISBN

0-7803-8253-6

Type

conf

DOI

10.1109/CCECE.2004.1349702

Filename

1349702