Specification of the RTPA grammar and its recognition

A new type of descriptive mathematics, real-time process algebra (RTPA), is developed for describing complicated behaviors of human beings and software systems. This paper describes the key syntax of RTPA defined by a set of 280 LL(k) grammar rules and their recognition techniques. The LL(k) grammar of RTPA is formally described by using the EBNF notations. The design of the RTPA parser and type checker are presented on the basis of the RTPA grammar. To deal with the special non-LL(k) grammar rules of RTPA, the ANTLR syntactic predicates are used to create guarded and extended rules. The tasks of type checking in RTPA recognition can be classified into three categories: (a) identifier type compliancy, (b) expression type compliancy, and (c) process constraint consistency. The implementation of the RTPA parser and type checker provides an important tool for RTPA recognition and for generating executable code for formal specifications of system architectures and behaviors in RTPA.