Converting BPSL Behavioral Specification to FSP Using A Java-Based
Toufik Taibi · 2003
Balanced Pattern Specification Language (BPSL) can be used to formally specify design patterns and their combination. BPSL uses a subset of First Order Logic (FOL) to specify the structural aspect of design patterns and a subset of Temporal Logic of Actions (TLA) to specify their behavioral aspect. BPSL as any other language requires a lexical analyzer (lexer) and a parser in order to allow its users to check the lexical and syntactic correctness of their specification. Writing lexers and parsers from scratch can be a tedious and error prone process. As such, lexers and parsers generation tools have been developed to automate this task. This paper describes how both Java-based Lexer (JLex) and Constructor of Useful Parsers (CUP) were successfully used to generate highly optimized Java-based lexer and parser for BPSL. Moreover CUP was used to convert BPSL behavioral specifications to the well-known Finite State Processes (FSP) specifications in order to use Labeled Transaction System Analyzer (LTSA) model checking tool.