DocumentCode
2304053
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
Volume
4
fYear
2009
fDate
19-21 May 2009
Firstpage
154
Lastpage
158
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;
fLanguage
English
Publisher
ieee
Conference_Titel
Software Engineering, 2009. WCSE '09. WRI World Congress on
Conference_Location
Xiamen
Print_ISBN
978-0-7695-3570-8
Type
conf
DOI
10.1109/WCSE.2009.317
Filename
5319523
Link To Document