NDLI: Epsilon-based model transformation and verification of train control system specification

Content Provider	IEEE Xplore Digital Library
Author	Liu Chao Tang Tao
Copyright Year	2011
Description	Author affiliation: State Key Laboratory of Rail Traffic Control and Safety, Beijing Jiaotong University, 100044, China (Liu Chao; Tang Tao)
Abstract	With the development of key technologies, train control system has become network-communicating safety related distributed system. In order to guarantee functions and performances of system meet the design requirements, it is essential to model and verify the specification during system development life cycle. The emergence of model transformation methodology in model-driven engineering bridges the gap between semi-formal modeling and formal verification, and builds links with model-based verification as well. This paper presents an approach to automatic model transformation and code generation atop Epsilon model management platform, and provides a case study of RBC hand-over scenarios described in train control system specification. In this case, system requirements are modeled via UML class and state machine diagram, which are then automatically transformed into SPIN/Promela formal language by means of model-model and model-text transformation via the ETL and EGL within Epsilon, to verify the correctness of hand-over design, accordingly the consistencies between system specification, functional design and model development are assured.
Starting Page	5562
Ending Page	5567
File Size	367995
Page Count	6
File Format	PDF
ISBN	9781457706776
ISSN	21612927
e-ISBN	9789881725592
Language	English
Publisher	Institute of Electrical and Electronics Engineers, Inc. (IEEE)
Publisher Date	2011-07-22
Publisher Place	China
Access Restriction	Subscribed
Rights Holder	Chinese Assoc of Automati
Subject Keyword	GSM Promela Unified modeling language UML Metals Epsilon Control systems Model transformation Electronic mail Safety Train Control System Formal verification
Content Type	Text
Resource Type	Article

Sl.	Authority	Responsibilities	Communication Details
1	Ministry of Education (GoI), Department of Higher Education	Sanctioning Authority	https://www.education.gov.in/ict-initiatives
2	Indian Institute of Technology Kharagpur	Host Institute of the Project: The host institute of the project is responsible for providing infrastructure support and hosting the project	https://www.iitkgp.ac.in
3	National Digital Library of India Office, Indian Institute of Technology Kharagpur	The administrative and infrastructural headquarters of the project	Dr. B. Sutradhar bsutra@ndl.gov.in
4	Project PI / Joint PI	Principal Investigator and Joint Principal Investigators of the project	Dr. B. Sutradhar bsutra@ndl.gov.in Prof. Saswat Chakrabarti will be added soon
5	Website/Portal (Helpdesk)	Queries regarding NDLI and its services	support@ndl.gov.in
6	Contents and Copyright Issues	Queries related to content curation and copyright issues	content@ndl.gov.in
7	National Digital Library of India Club (NDLI Club)	Queries related to NDLI Club formation, support, user awareness program, seminar/symposium, collaboration, social media, promotion, and outreach	clubsupport@ndl.gov.in
8	Digital Preservation Centre (DPC)	Assistance with digitizing and archiving copyright-free printed books	dpc@ndl.gov.in
9	IDR Setup or Support	Queries related to establishment and support of Institutional Digital Repository (IDR) and IDR workshops	idr@ndl.gov.in

Formal verification of UML-modeled machine controls

Petri nets and Activity Diagrams in logic controller specification - transformation and verification

UML Modeling and Formal Verification of Control/Data Driven Embedded Systems

Model Transformation Specification and Verification

Model transformation specification for automated formal verification

Model-based verification in the development of dependable systems

Formal specification and automated verification of UML2.0 sequence diagrams

Property Specification and Static Verification of UML Models

Correct Transformation . . . Promela for verification (2011)

Epsilon-based model transformation and verification of train control system specification

Similar Documents

Formal verification of UML-modeled machine controls

Petri nets and Activity Diagrams in logic controller specification - transformation and verification

UML Modeling and Formal Verification of Control/Data Driven Embedded Systems

Model Transformation Specification and Verification

Model transformation specification for automated formal verification

Model-based verification in the development of dependable systems

Formal specification and automated verification of UML2.0 sequence diagrams

Property Specification and Static Verification of UML Models

Correct Transformation . . . Promela for verification (2011)

Epsilon-based model transformation and verification of train control system specification