Speaker: Jianwei Niu , School of Computer Science, University of Waterloo
Metro: A Semantics-Based Approach for Mapping Specification Notations to Analysis Tools
Abstract: We propose a semantics-based approach, Metro, to generate analyzers automatically from the description of notations' semantics. In Metro, the semantics of a notation are defined and fed into a model compiler together with a specification in that notation. A transition-relation for the specification is generated automatically, which can be checked using many automatic analysis tools (e.g., model checkers). However, the semantics of many model-based notations (e.g., statecharts and process algebras) are complex and formalizing their semantics can be challenging and error-prone.
To ease the effort required to define the semantics, we have developed an operational semantics template that captures the common behaviour of different notations and parameterizes notations' distinct behaviours. We have also identified seven well-used composition operators and defined the semantics of these operators separately, as relations that constrain how components can execute concurrently, and communicate and synchronize with each other by exchanging events and data. By separating a notation's step-semantics from its composition and concurrency operators, we simplify the definitions of both. We have used our template to capture the essential semantics of basic transition systems, CSP, CCS, basic LOTOS, a subset of SDL88, and a variety of statecharts notations.
Short Bio: Jianwei Niu received the BSc degree in computer science from Jilin University, Changchun, China. She is a PhD candidate in the School of Computer Science at the University of Waterloo. She is a member of the Waterloo Formal Methods (WatForm) research group. Her research interests include formal methods and requirements engineering. She is a student member of the ACM, ACM SIGSOFT, and the IEEE.
Host: Purush Iyer, Computer Science, NCSU