Seminars & Meetings | Abstracts

Wednesday, January 25, 2012

Levine 307, 2 pm - 3 pm

Nguyen Van Tang
Postdoc Researcher, Research Center for Verification and Specification
National Institute of Advanced Industrial Science and Technology

Modeling and Validating the Train Fare Calculation and
Adjustment System Using VDM++


The Train Fare Calculation and Adjustment System (TFCAS), developed by the OMRON Corporation, is a large-scale and complex system that helps passengers buy tickets and adjust their train fare on the railways across Japan. In this paper we present the results and experiences gained in a collaborative research project between AIST and OMRON, in which VDM++ has been applied to formalize TFCAS's specifications and validate its consistency as well as reliability properties. An executable VDM++ model can be used to raise the level of the quality of the informal system specification, the efficiency of existing system test-suites, and the quality of real implementation. The application of VDM++ enables us to detect 32 erroneous issues in the original informal specification document. Moreover, we also show how the development process can be improved in a front-loading manner using the formal method VDM++.

Research Interests:
  • Formal Methods, Software Verification and Validation
  • Real-time Systems, Hybrid Systems, Embedded Systems
  • Temporal Logic, Model Checking, Theorem Proving, SAT/SMT Solvers
  • Logics and Validation for XML