Symbolic model-checking of stateful timed CSP using BDD and digitization

• Main Authors: NGUYEN, Truong Khanh, SUN, Jun, LIU, Yang, DONG, Jin Song
• 格式: text
• 語言: English
• 出版: Institutional Knowledge at Singapore Management University 2012
• 主題: Model Check; Compositional Function; Linear Temporal Logic; Model Check Algorithm; State Space Explosion; Programming Languages and Compilers; Software Engineering
• 在線閱讀: https://ink.library.smu.edu.sg/sis_research/5024; https://ink.library.smu.edu.sg/context/sis_research/article/6027/viewcontent/symbolic.pdf

Stateful Timed CSP has been recently proposed to model (and verify) hierarchical real-time systems. It is an expressive modeling language which combines data structure/operations, complicated control flows (modeled using compositional process operators adopted from Timed CSP), and real-time requirem...