Wyniki wyszukiwania - BazTech

Ograniczanie wyników

Znaleziono wyników: 4

Liczba wyników na stronie

Wyniki wyszukiwania

Wyszukiwano:
w słowach kluczowych: ECTL

Sortuj według:

Ogranicz wyniki do:

Comparing sat-based bounded model checking rtectl and ectl properties

Zbrzezny A. M.

Technical Sciences / University of Warmia and Mazury in Olsztyn

2017

nr 20(2)

131--147

We compare two SAT-based bounded model checking algorithms for the properties expressed in the existential fragment of a soft real-time computation tree logic (RTECTL) and in the existential fragment of computation tree logic (ECTL). To this end, we use the generic pipeline paradigm (GPP) and the train controller system (TC), the classic concurrency problems, which we formalise by means of a finite transition system. We consider several properties of the problems that can be expressed in both RTECTL and ECTL, and we present the performance evaluation of the mentioned bounded model checking methods by means of the running time and the memory used.

A New Translation from ECTL* to SAT*

Zbrzezny A.

Fundamenta Informaticae

2012

Vol. 120, nr 3/4

375-395

In this paper we present a new translation from ECTL* to SAT and show that the proposed translation substantially increases the efficiency of verifying temporal properties using the Bounded Model Checking method. We have implemented our new translation and made experimental results, which demonstrate the efficiency of the method.

Improving the Translation from ECTL to SAT

Zbrzezny A.

Fundamenta Informaticae

2008

Vol. 85, nr 1-4

513-531

The objective of this paper is to offer an improvement to the translation from ECTL to SAT introduced in [14] and show that the improvement proposed substantially increases the efficiency of verifying temporal properties using the Bounded Model Checking method. We have implemented our new translation and made preliminary experimental results, which demonstrate the efficiency of the method.

ACTL* properties and Bounded Model Checking

Woźna B.

Fundamenta Informaticae

2004

Vol. 63, nr 1

65--87

The main contribution of the paper consists in showing that the bounded model checking (BMC) method is feasible for ACTL* (the universal fragment of CTLS) which subsumes both ACTL and LTL. The extension to ACTL* is obtained by redefining the function returning the sufficient number of executions over which an ACTL* formula is checked, and then combining the two known translations to SAT for ACTL and LTL formulas. The proposed translation of ACTL* formulas is essentially different from the existing translations of both ACTL and LTL formulas. Moreover, the formal treatment is the basis for the implementation of the technique in the symbolic model checker Verics.