Wyniki wyszukiwania - BazTech

Ograniczanie wyników

Znaleziono wyników: 2

Liczba wyników na stronie

Wyniki wyszukiwania

Wyszukiwano:
w słowach kluczowych: translating

Sortuj według:

Ogranicz wyniki do:

Declarative Parameterized Verification of Distributed Protocols via the Cubicle Model Checker

Conchon Sylvain, Delzanno Giorgio, Ferrando Angelo

Fundamenta Informaticae

2021

Vol. 178, nr 4

347--378

We show that Cubicle, an SMT-based infinite-state model checker, can be applied as a verification engine for GLog, a logic-based language based on relational updates rules that has been applied to specify topology-sensitive distributed protocols with asynchronous communication. In this setting, the absence of protocol anomalies can be reduced to a coverability problem in which the initial set of configurations is not fixed a priori (Existential Coverability Problem). Existential Coverability in GLog can naturally be expressed into Parameterized Verification judgements in Cubicle. The encoding is based on a translation of relational update rules into transition rules that modify cells of unbounded arrays. To show the effectiveness of the approach, we discuss several verification problems for distributed protocols and distributed objects, a challenging task for traditional verification tools. The experimental results show the flexibility and robustness of Cubicle for the considered class of protocol examples.

Expert judgement in safety prediction by the methodology of I Cing language.

Smalko Z., Nowakowski T.

Systems : journal of transdisciplinary systems science

2000

Vol. 5, No. 1-2

88-95

The possibilities of I Cing language use as an expert knowledge base for a man safety prediction are discussed. The analysis of the I Cing is done according to the formal attributes of a knowledge base. The inference process is divided into 3 stages: a hexagram value statement, choice of a commentary and interpretation of commentary. Some of translating the language expression or metaphors into the vocabulary used in machines operation and safety are shown.