Wyniki wyszukiwania - BazTech

Ograniczanie wyników

2 2020

Znaleziono wyników: 2

Liczba wyników na stronie

Wyniki wyszukiwania

Wyszukiwano:
w słowach kluczowych: symbolic execution

Sortuj według:

Ogranicz wyniki do:

Abstract Contract Synthesis and Verification in the Symbolic 𝕂 Framework

Alpuente Maria, Pardo Daniel, Villanueva Alicia

Fundamenta Informaticae

2020

Vol. 177, nr 3/4

235--273

In this article, we propose a symbolic technique that can be used for automatically inferring software contracts from programs that are written in a non-trivial fragment of C, called KERNEL C, that supports pointer-based structures and heap manipulation. Starting from the semantic definition of KERNEL C in the 𝕂 semantic framework, we enrich the symbolic execution facilities recently provided by 𝕂 with novel capabilities for contract synthesis that are based on abstract subsumption. Roughly speaking, we define an abstract symbolic technique that axiomatically explains the execution of any (modifier) C function by using other (observer) routines in the same program. We implemented our technique in the automated tool KIND SPEC 2.1, which generates logical axioms that express pre- and post-condition assertions which define the precise input/output behavior of the C routines. Thanks to the integrated support for symbolic execution and deductive verification provided by 𝕂, some synthesized axioms that cannot be guaranteed to be correct by construction due to abstraction can finally be verified in our setting with little effort.

Data Quality Model-based Testing of Information Systems

Bicevskis Janis, Bicevska Zane, Nikiforova Anastasija, Oditis Ivo

Annals of Computer Science and Information Systems

2020

Vol. 21

595--602

This paper proposes a model-based testing approach by offering to use the data quality model (DQ-model) instead of the program's control flow graph as a testing model. The DQ-model contains definitions and conditions for data objects to consider the data object as correct. The study proposes to automatically generate a complete test set (CTS) using a DQ-model that allows all data quality conditions to be tested, resulting in a full coverage of DQ-model. In addition, the possibility to check the conformity of the data to be entered and already stored in the database is ensured. The proposed alternative approach changes the testing process: (1) CTS can be generated prior to software development; (2) CTS contains not only input data, but also database content required for complete testing of the system; (3) CTS generation from DQ-model provides values against which the system can be further tested. If the test results correspond to the values obtained during CTS generation, the system under test shall be considered to have been tested according to DQ-model. Otherwise, the user can verify the cause of the differences that may occur due incorrect software, as well as an inaccurate specification.