Integrated Specification, Validation and Verification with HybridUML and OCL applied to the BART Case Study

Authors

Stefan Bisanz, Paul Ziemann, and Arne Lindow

Abstract

This article proposes the integration of the HybridUML specification formalism and the USE approach for validation of invariant constraints and verification of system states. The benefit is an executable real-time simulation with an integrated verification/validation component, which combines the advantages of the previously separate approaches by providing an accurate, (partially) time-continuous model that can be checked for consistency between static invariants and dynamical behavior in terms of a complete UML model. The integration is illustrated by means of a train system specification - the BART case study.

Full Article

Download the full article: pdf format (4 MB) or gzipped pdf format (1.8 MB) or gzipped ps format (1.3 MB)

Published in:

E. Schnieder, and G. Tarnai, editors: FORMS/FORMAT 2004. Formal Methods for Automation and Safety in Railway and Automotive Systems, Proceedings of Symposium FORMS/FORMAT 2004, Braunschweig, Germany, 2^nd and 3^rd December 2004. ISBN 3-9803363-8-7.

Presentation Slides

pdf (3.6 MB) or gzipped pdf (1.6 MB), presented at "FORMS/FORMAT 2004. Formal Methods for Automation and Safety in Railway and Automotive Systems", 5. Symposium, in Braunschweig, Germany, 03.12.2004

Together Designer CE Model

The HybridUML/OCL model is available as zip archive. It requires the tool Together Designer from Borland Software Corporation. The model was created with tool version "Together Designer Community Edition Version 1.0".

Author: alien

AG BS

Last updated: November 2, 2022