Wyniki wyszukiwania - BazTech

Ograniczanie wyników

Znaleziono wyników: 2

Liczba wyników na stronie

Wyniki wyszukiwania

Wyszukiwano:
w słowach kluczowych: RTECTL

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.

Verifying RTECTL properties of a train controller systems

Woźna-Szcześniak B., Zbrzezny A., Zbrzezny Andrzej

Scientific Issues of Jan Długosz University in Częstochowa. Mathematics

2011

Vol. 16

153--162

In the paper we deal with a classic concurrency problem - a faulty train controller system (FTC). In particular, we formalize it by means of finite automata, and consider several properties of the problem, which can be expressed as formulae of a soft real-time branching time temporal logic, called RTECTL. Further, we verify the RTECTL properties of FTC by means of SAT-based bounded model checking (BMC) method, and present the performance evaluation of the BMC method with respect to the considered problem. The performance evaluation is given by means of the running time and the memory used.