Journal of Systems Engineering and Electronics ›› 2011, Vol. 33 ›› Issue (2): 458-463.doi: 10.3969/j.issn.1001-506X.2011.02.45
Previous Articles Next Articles
LI Zhen, LIU Bin, LI Xiao-xun, YIN Yong-feng
Online:
Published:
Abstract:
It is very beneficial to apply formal modeling and model checking to improve the dependability of safety-critical software, but there are limitations in model description, debugging and explanation. The extension of Petri-net to model the software system and the default value of weight functions to zero are set up, the fire under false state or failed transition by a “Not” dotted line is described, the ability to describe the condition of threshold is enhanced. This paper differentiates between enumeration place and numeric place, between normal transition and valueassigned transition. The formal definition of extended Petri net and its semantic mapping to verification language are given. Finally, the application in airborne engine software to build the software requirement model and the mapping code for verification, counterexample analysis and improvement are given. The process and result show the methodology can effectively support the safety-critical software requirement modeling and verification in practice.
CLC Number:
TP 311.5
LI Zhen, LIU Bin, LI Xiao-xun, YIN Yong-feng. Verification of safetycritical software requirement based on Petri-net model checking[J]. Journal of Systems Engineering and Electronics, 2011, 33(2): 458-463.
0 / / Recommend
Add to citation manager EndNote|Reference Manager|ProCite|BibTeX|RefWorks
URL: https://www.sys-ele.com/EN/10.3969/j.issn.1001-506X.2011.02.45
https://www.sys-ele.com/EN/Y2011/V33/I2/458