Converting BPSL Behavioral Specification to FSP Using A Java-Based Parser Generator

 

Toufik Taibi

Faculty of Information Technology
Multimedia University

Jalan Multimedia, 63100 Cyberjaya
Selangor, Malaysia

toufik.taibi@mmu.edu.my

 

 

Abstract

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.

 

Keywords: BPSL, Lexer, Parser, JLex, CUP, FSP, LTSA