Modeling and verifying hierarchical real-time systems using stateful timed CSP

Modeling and verifying complex real-time systems are challenging research problems. The de facto approach is based on Timed Automata, which are finite state automata equipped with clock variables. Timed Automata are deficient in modeling hierarchical complex systems. In this work, we propose a langu...

Full description

Saved in:
Bibliographic Details
Main Authors: SUN, Jun, LIU, Yang, DONG, Jin Song, LIU, Yan, SHI, Ling, ANDRÉ, Étienne
Format: text
Language:English
Published: Institutional Knowledge at Singapore Management University 2013
Subjects:
Online Access:https://ink.library.smu.edu.sg/sis_research/4995
https://ink.library.smu.edu.sg/context/sis_research/article/5998/viewcontent/2430536.2430537.pdf
Tags: Add Tag
No Tags, Be the first to tag this record!
Institution: Singapore Management University
Language: English
id sg-smu-ink.sis_research-5998
record_format dspace
spelling sg-smu-ink.sis_research-59982020-03-12T09:41:03Z Modeling and verifying hierarchical real-time systems using stateful timed CSP SUN, Jun LIU, Yang DONG, Jin Song LIU, Yan SHI, Ling ANDRÉ, Étienne Modeling and verifying complex real-time systems are challenging research problems. The de facto approach is based on Timed Automata, which are finite state automata equipped with clock variables. Timed Automata are deficient in modeling hierarchical complex systems. In this work, we propose a language called Stateful Timed CSP and an automated approach for verifying Stateful Timed CSP models. Stateful Timed CSP is based on Timed CSP and is capable of specifying hierarchical real-time systems. Through dynamic zone abstraction, finite-state zone graphs can be generated automatically from Stateful Timed CSP models, which are subject to model checking. Like Timed Automata, Stateful Timed CSP models suffer from Zeno runs, that is, system runs that take infinitely many steps within finite time. Unlike Timed Automata, model checking with non-Zenoness in Stateful Timed CSP can be achieved based on the zone graphs. We extend the PAT model checker to support system modeling and verification using Stateful Timed CSP and show its usability/scalability via verification of real-world systems. 2013-01-02T08:00:00Z text application/pdf https://ink.library.smu.edu.sg/sis_research/4995 info:doi/10.1145/2430536.2430537 https://ink.library.smu.edu.sg/context/sis_research/article/5998/viewcontent/2430536.2430537.pdf http://creativecommons.org/licenses/by-nc-nd/4.0/ Research Collection School Of Computing and Information Systems eng Institutional Knowledge at Singapore Management University Algorithms Languages Verification Programming Languages and Compilers Software Engineering
institution Singapore Management University
building SMU Libraries
continent Asia
country Singapore
Singapore
content_provider SMU Libraries
collection InK@SMU
language English
topic Algorithms
Languages
Verification
Programming Languages and Compilers
Software Engineering
spellingShingle Algorithms
Languages
Verification
Programming Languages and Compilers
Software Engineering
SUN, Jun
LIU, Yang
DONG, Jin Song
LIU, Yan
SHI, Ling
ANDRÉ, Étienne
Modeling and verifying hierarchical real-time systems using stateful timed CSP
description Modeling and verifying complex real-time systems are challenging research problems. The de facto approach is based on Timed Automata, which are finite state automata equipped with clock variables. Timed Automata are deficient in modeling hierarchical complex systems. In this work, we propose a language called Stateful Timed CSP and an automated approach for verifying Stateful Timed CSP models. Stateful Timed CSP is based on Timed CSP and is capable of specifying hierarchical real-time systems. Through dynamic zone abstraction, finite-state zone graphs can be generated automatically from Stateful Timed CSP models, which are subject to model checking. Like Timed Automata, Stateful Timed CSP models suffer from Zeno runs, that is, system runs that take infinitely many steps within finite time. Unlike Timed Automata, model checking with non-Zenoness in Stateful Timed CSP can be achieved based on the zone graphs. We extend the PAT model checker to support system modeling and verification using Stateful Timed CSP and show its usability/scalability via verification of real-world systems.
format text
author SUN, Jun
LIU, Yang
DONG, Jin Song
LIU, Yan
SHI, Ling
ANDRÉ, Étienne
author_facet SUN, Jun
LIU, Yang
DONG, Jin Song
LIU, Yan
SHI, Ling
ANDRÉ, Étienne
author_sort SUN, Jun
title Modeling and verifying hierarchical real-time systems using stateful timed CSP
title_short Modeling and verifying hierarchical real-time systems using stateful timed CSP
title_full Modeling and verifying hierarchical real-time systems using stateful timed CSP
title_fullStr Modeling and verifying hierarchical real-time systems using stateful timed CSP
title_full_unstemmed Modeling and verifying hierarchical real-time systems using stateful timed CSP
title_sort modeling and verifying hierarchical real-time systems using stateful timed csp
publisher Institutional Knowledge at Singapore Management University
publishDate 2013
url https://ink.library.smu.edu.sg/sis_research/4995
https://ink.library.smu.edu.sg/context/sis_research/article/5998/viewcontent/2430536.2430537.pdf
_version_ 1770575186352930816