Publication Type

Journal Article

Version

publishedVersion

Publication Date

1-2014

Abstract

Modeling and verifying complex real-time systems, involving timing delays, are notoriously difficult problems. Checking the correctness of a system for one particular value for each delay does not give any information for other values. It is thus interesting to reason parametrically, by considering that the delays are parameters (unknown constants) and synthesizing a constraint guaranteeing a correct behavior. We present here Parametric Stateful Timed Communicating Sequential Processes, a language capable of specifying and verifying parametric hierarchical real-time systems with complex data structures. Although we prove that the synthesis is undecidable in general, we present several semi-algorithms for efficient parameter synthesis, which behave well in practice. This work has been implemented in a real-time model checker, PSyHCoS, and validated on a set of case studies.

Keywords

Real-time specification, Parametric timed verification, Model checking, Robustness

Discipline

Programming Languages and Compilers | Software Engineering

Research Areas

Software and Cyber-Physical Systems

Publication

Real-Time Systems

Volume

50

Issue

5-6

First Page

620

Last Page

679

ISSN

0922-6443

Identifier

10.1007/s11241-014-9208-6

Publisher

Springer Verlag (Germany)

Additional URL

https://doi.org/10.1007/s11241-014-9208-6

Download

Share

COinS