PSyHCoS: Parameter synthesis for hierarchical concurrent real-time systems

• Main Authors: ANDRÉ, Étienne, LIU, Yang, SUN, Jun, DONG, Jin Song, LIN, Shang-Wei
• Format: text
• Language: English
• Published: Institutional Knowledge at Singapore Management University 2013
• Subjects: Model Check; Mutual Exclusion Label Transition System Parameter Synthesis Reference Valuation; Software Engineering
• Online Access: https://ink.library.smu.edu.sg/sis_research/4958; https://ink.library.smu.edu.sg/context/sis_research/article/5961/viewcontent/PSyHCoS.pdf
• Institution: Singapore Management University

Real-time systems are often hard to control, due to their complicated structures, quantitative time factors and even unknown delays. We present here PSyHCoS, a tool for analyzing parametric real-time systems specified using the hierarchical modeling language PSTCSP. PSyHCoS supports several algorithms for parameter synthesis and model checking, as well as state space reduction techniques. Its architecture favors reusability in terms of syntax, semantics, and algorithms. It comes with a friendly user interface that can be used to edit, simulate and verify PSTCSP models. Experiments show its efficiency and applicability