Software Trustworthiness Mesurement Based On Model Checking

In the21st century, software is taking important role in all part of society, frombasic life necessities to a variety of key positions, there are different soft wares whichassist human in automated manipulation. However, due to the increasing complexity,the number of software defects is growing, from the "Millennium Bug" to "Apollo"spacecraft crash accident, many kinds of software errors or failure event appears,software is difficult to trust. It is urgent to provide a key technology of the softwaretrustworthy measurement.Software trustworthiness measurement is to measure the extent of software actsas expected purpose. Model checking is a kind of automatic formal verificationmethod, it is able to automatically and verify that the system meets the appropriatenature. Model checking is faster, accurate and automated,This paper summarized and analyzed existing software measurement methodsand finished research work in the following three aspects:First, raised a kind of software trustworthiness measurement method based onmodel checking of UML activity diagram with model checking tool SPIN. UMLactivity diagram is modeled into state system using PROMELA description language,the trustworthy property is converted to LTL temporal logic, then set them as SPIN’sinput, given the software trustworthiness measurement results, analysis software’strustworthiness in the early stage of software development;Second, raised a kind of software trustworthiness measurement method based onmodel checking of source codes with model checking tool MOPS. Source codes areextracted and transferred into PDA automation, also the trustworthiness properties areconverted in to FSA, then enter them into MOPS and verify software trustworthinessin coding stage.Third, against existing software trustworthiness measurement problems raised akind of software trustworthiness measurement model based on software life cyclemodel. The model combined formal methods and non-formal methods in software lifecycle and can give comprehensive and accurate reflection of software trustworthiness.