scholarly journals Expert Assessment of Verification Tool Results

2020 ◽  
Vol 32 (5) ◽  
pp. 7-20
Author(s):  
Vladimir Anatolyevich Gratinskiy ◽  
Evgeny Mikhailovich Novikov ◽  
Ilja Sergeevich Zakharov
Keyword(s):  
Software Verification ◽  
Expert Assessment ◽  
Expert Evaluation ◽  
Code Coverage ◽  
New Methods ◽  
Requirements Specifications ◽  
Verification Tool ◽  
Verification Tools ◽  
Technical Solutions ◽  
Requirement Specifications

Verification tools can produce various kinds of results while checking programs against requirement specifications. Experts, who seek for errors and estimate completeness of verification, mostly appreciate verdicts, violation witnesses and code coverage reports. They need convenient tools for automating the assessment of verification results to apply verification tools in practice when many program configurations and versions are checked against various requirements. In this paper, we propose new methods for expert evaluation of verification results, covering all those problems that are most significant in accordance with our experience in verifying large programs for compliance with a large number of requirements specifications. Some ideas are borrowed from the areas of testing and static analysis. However, specific methods and technical solutions are unique, since the verification results provided by verification tools are either not found in other areas or have special semantics. The paper presents our approaches and their implementation in the Klever software verification framework.

scholarly journals CoVEGI: Cooperative Verification via Externally Generated Invariants

2021 ◽  
pp. 108-129
Author(s):  
Jan Haltermann ◽  
Heike Wehrheim
Keyword(s):  
Software Verification ◽  
Black Box ◽  
Loop Invariant ◽  
Invariant Generation ◽  
Smt Solving ◽  
The Core ◽  
Verification Tool ◽  
Verification Methods ◽  
Speed Up ◽  
Verification Tools

AbstractSoftware verification has recently made enormous progress due to the development of novel verification methods and the speed-up of supporting technologies like SMT solving. To keep software verification tools up to date with these advances, tool developers keep on integrating newly designed methods into their tools, almost exclusively by re-implementing the method within their own framework. While this allows for a conceptual re-use of methods, it nevertheless requires novel implementations for every new technique.In this paper, we employ cooperative verification in order to avoid re-implementation and enable usage of novel tools as black-box components in verification. Specifically, cooperation is employed for the core ingredient of software verification which is invariant generation. Finding an adequate loop invariant is key to the success of a verification run. Our framework named CoVEGI allows a master verification tool to delegate the task of invariant generation to one or several specialized helper invariant generators. Their results are then utilized within the verification run of the master verifier, allowing in particular for crosschecking the validity of the invariant. We experimentally evaluate our framework on an instance with two masters and three different invariant generators using a number of benchmarks from SV-COMP 2020. The experiments show that the use of CoVEGI can increase the number of correctly verified tasks without increasing the used resources.

scholarly journals Invariants and Robustness of BIP Models

10.29007/prxp ◽  
2018 ◽  
Author(s):  
Jan Olaf Blech ◽  
Thanh-Hung Nguyen ◽  
Michael Perin
Keyword(s):  
Embedded Systems ◽  
Higher Order ◽  
Theorem Prover ◽  
Important Goal ◽  
Invariant Generation ◽  
Execution Traces ◽  
Verification Tool ◽  
Verification Tools ◽  
Generation Mechanisms ◽  
Natural Way

In this paper we present on-going work addressing the problem of automatically generating realistic and guaranteed correct invariants. Since invariant generation mechanisms are error-prone, after the computation of invariants by a verification tool, we formally prove that the generated invariants are indeed invariants of the considered systems using a higher-order theorem prover and automated techniques. We regard invariants for BIP models. BIP (behavior, interaction, priority) is a language for specifying asynchronous component based systems. Proving that an invariant holds often requires an induction on possible system execution traces. For this reason, apart from generating invariants that precisely capture a system’s behavior, inductiveness of invariants is an important goal. We establish a notion of robust BIP models. These can be automatically constructed from our original non-robust BIP models and over-approximate their behavior. We motivate that invariants of robust BIP models capture the behavior of systems in a more natural way than invariants of corresponding non-robust BIP models. Robust BIP models take imprecision due to values delivered by sensors into account. Invariants of robust BIP models tend to be inductive and are also invariants of the original non-robust BIP model. Therefore they may be used by our verification tools and it is easy to show their correctness in a higher-order theorem prover. The presented work is developed to verify the results of a deadlock-checking tool for embedded systems after their computations. Therewith, we gain confidence in the provided analysis results.

scholarly journals Making Software Verification Tools Really Work

2011 ◽  
pp. 28-42 ◽  
Author(s):  
Jade Alglave ◽  
Alastair F. Donaldson ◽  
Daniel Kroening ◽  
Michael Tautschnig
Keyword(s):  
Software Verification ◽  
Verification Tools

EXPERT EVALUATION OF WEB-BASED SYSTEMS BASED ON THE LINGUISTIC APPROACH

2021 ◽  
pp. 14-18
Author(s):  
М.Ю. Сергеев ◽  
Т.И. Сергеева ◽  
Н.И. Гребенникова
Keyword(s):  
Quality Indicators ◽  
Evaluation System ◽  
Expert Assessment ◽  
Expert Evaluation ◽  
Linguistic Terms ◽  
Web Based ◽  
Main Indicator ◽  
Development Goals ◽  
Consistent Assessment ◽  
Linguistic Approach

Рассмотрен подход к оценке результатов разработки веб-ориентированных систем в рамках экспертных систем на основе применения лингвистического подхода. Рассмотрены особенности формирования интегральных показателей качества функционирования и эксплуатации веб-ориентированных систем. Показан способ формализации требований экспертов к веб-ориентированным системам. Оценка эксплуатационных характеристик строится на основе формирования лингвистических шкал, позволяющих оценить качественные показатели, не имеющиe количественной оценки. Приведены примеры лингвистических термов для оценки разнообразных показателей работы веб-ориентированных систем. Приведено соответствие между уточняющими показателями качества разработанной системы и лингвистическими термами. Рассмотрен подход к переходу от качественных показателей к количественным частотным характеристикам. Экспертная система обеспечивает учет неопределенности в оценке веб-проектов и базируется на формализации неточной и нечеткой информации. Предложенный подход к формированию экспертной системы оценки разработанной веб-ориентированной системы обеспечивает согласованную оценку разработанной системы с помощью группы интегральных показателей качества. Экспертная оценка позволит определить соответствие реализации проекта поставленным целям разработки, что, в свою очередь, даст возможность установить, насколько будет успешной финансовая составляющая деятельности компании, что является главным показателем эффективности The article considers an approach to evaluating the results of the development of web-oriented systems in the framework of expert systems based on the use of a linguistic approach. It discusses the features of the formation of integral indicators of the quality of functioning and operation of web-oriented systems. We show the method of formalizing the requirements of experts for web-based systems. The evaluation of operational characteristics is based on the formation of linguistic scales that allow one to evaluate qualitative indicators that do not have a quantitative assessment. We give examples of linguistic terms for evaluating various performance indicators of web-oriented systems and also we give the correspondence between the clarifying quality indicators of the developed system and the linguistic terms. We considered an approach to the transition from qualitative indicators to quantitative frequency characteristics. The expert system takes into account the uncertainty in the evaluation of web projects and is based on the formalization of inaccurate and fuzzy information. The proposed approach to the formation of an expert evaluation system of the developed web-based system provides a consistent assessment of the developed system with the help of a group of integral quality indicators. The expert assessment will determine the compliance of the project implementation with the set development goals, which, in turn, will make it possible to determine how successful the financial component of the company's activities will be, which is the main indicator of efficiency

Sign in / Sign up

Export Citation Format

Share Document