Type checking for software system specifications in real-time process algebra

This paper presents the development of 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 allows it be easily parsed as well. 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. And it shows that with the grammar defined, the type checker can be integrated with the parser and do both parsing and type checking in one pass.