Title :
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
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;
Conference_Titel :
Electrical and Computer Engineering, 2004. Canadian Conference on
Print_ISBN :
0-7803-8253-6
DOI :
10.1109/CCECE.2004.1349702
