Title :
Verification Framework of Scenario-Based Safety Requirement
Author :
Junwei, Du ; Guozhu, Liu
Author_Institution :
Sch. of Inf. Sci. & Technol., Qingdao Univ. of Sci. & Technol., Qingdao, China
Abstract :
Light-weight formal verification framework, based on CRA, focusing on industry application is proposed in this paper, which safety requirements specification, described by PSC(property sequence chart), can be automatic transformed into LTS(labeled transition system). We present the translation algorithm from PSC to image LTS, by proving that the PSC semantic can be transformed into linearization sequences set. Thus, safety requirement specifications can be verified by CRA and be implemented by LTSA tools.
Keywords :
formal verification; CRA focusing; PSC; labeled transition system; light-weight formal verification framework; linearization sequences set; property sequence chart; scenario-based safety requirement; translation algorithm; Formal specifications; Formal verification; Industrial relations; Industry applications; Information science; Logic; Software algorithms; Software engineering; Software safety; Unified modeling language; CRA; LTS; PSC; safety requirement;
Conference_Titel :
Software Engineering, 2009. WCSE '09. WRI World Congress on
Conference_Location :
Xiamen
Print_ISBN :
978-0-7695-3570-8
DOI :
10.1109/WCSE.2009.317
