PROOF INDEPENDENT VERIFICATION AND FORECASTING OF THE HIDDEN DEFECTS OF CRITICAL SOFTWARE BASED MEASUREMENT DIVERSITY INVARIANTS
Keywords:
Software, verification formal methods, testing, independent verification, invariant, calibration profile defects.Abstract
Dependability and Safety of instrumentation and control critical systems depend on characteristics of quality of the software, performing critical functions. Latent faults (faults undetected during testing or verification) of the critical software are factors of the risk of system failure. The independent verification of the critical software, which confirms a performance of declared functions and estimates a probability of latent faults existence, is the necessary condition according to the regulative requirements for different areas (IAEA, ESA and so on). From this point of view, the main problems are: the reliability of independent verification; assessment of latent faults probability; completeness of test coverage for the critical software and as result the quantitative assessment of functional safety. Considered is the development and implementation of the advanced methodology of proven independent verification on the base of the software sourcecode static analysis. Methodology is aimed at the assessment of the semantic, intervalprecision, logic and others invariants ((software properties invariable during the life cycle)) of critical software and also generation and presentations of results of assessment conformity to requirements of standards and project specifications.References
Конорев Б.М. Инварианто-ориентированная оценка качества программного обеспечения космических систем/ Конорев Б.М., Харченко В.С., Алексеев Ю.Г., Манжос Ю.С., Сергиенко В.В., Чертков Г.Н. / Монография. Под ред. Конорева Б.М., Харченко В.С. – Харьков: ГП Госцентркачества, Национальный аэрокосмический университет им. Н.Е. Жуковского «ХАИ», 2009. – 224 с.
Кларк Э.М. Верификация моделей программ: Model Checking / Э.М. Кларк, О. Грамберг, Д. Пелед Пер. с англ. / Под ред. Р. Смелянского. — М.: МЦНМО, 2002. – 416 с.
Конорев Б.М., Сергиенко В.В., Новы Л., Чертков Г.Н. Калибровка методов измерения инвариантов критического программного обеспечения: профиль инъектируемых тестовых дефектов// Радіоелектронні і комп’ютерні системи. Науково-технічний журнал №6 (25), Харків, "ХАІ" 2008. – с.161 – 167 (ISSN 1814-4225).
IEC 60880 ed2:2006. Nuclear power plants – Instrumentation and Control systems important for safety – Software aspects for computer-based systems performing category А functions.
IEC 62138:2004. Nuclear power plants – Instrumentation and Control systems important for safety – Software aspects for computer-based systems performing category B and C functions.