PL
 |
EN
Preferencje help
Polish version English version Język
Widoczny [Schowaj] Abstrakt
Liczba wyników

Znaleziono wyników: 28

Liczba wyników na stronie
first rewind previous Strona / 2 next fast forward last
Wyniki wyszukiwania
Wyszukiwano:
w słowach kluczowych:  temporal logic
help Sortuj według:

help Ogranicz wyniki do:
first rewind previous Strona / 2 next fast forward last
1
Content available Model Checking Temporal Properties of Reaction Systems
Męski A., Penczek W., Rozenberg G.
Prace Instytutu Podstaw Informatyki Polskiej Akademii Nauk
|
2014
|
Nr 1028
1--28
EN
This paper defines a temporal logic for reaction systems (RSTL). The logic is interpreted over the models for the context restricted reaction systems that generalize standard reaction systems by controlling context sequences. Moreover, a translation from the context restricted reaction systems into boolean functions is defined in order to be used for a symbolic model checking for RSTL over these systems. Finally, model checking for RSTL is proved to be PSPACE-complete.
PL
Praca wprowadza logikę temporalną dla systemów reakcyjnych (RSTL), która jest interpretowana w modelach dla systemów reakcyjnych z ograniczeniami kontekstów. Systemy te uogólniają standardowe systemy reakcyjne przez wprowadzenie ograniczeń kontrolujących dopuszczalne konteksty. Ponadto, przedstawiono translację z systemów reakcyjnych z ograniczeniami kontekstów do formuł boolowskich, która umożliwia symboliczną weryfikację modelową dla tych systemów oraz RSTL. Wykazano również, że problem weryfikacji modelowej dla RSTL jest problemem PSPACE-zupełnym.
2
Content available A system for deduction-based formal verification of workflow-oriented software models
Klimek R.
International Journal of Applied Mathematics and Computer Science
|
2014
|
Vol. 24, no. 4
941--956
EN
The work concerns formal verification of workflow-oriented software models using the deductive approach. The formal correctness of a model’s behaviour is considered. Manually building logical specifications, which are regarded as a set of temporal logic formulas, seems to be a significant obstacle for an inexperienced user when applying the deductive approach. A system, along with its architecture, for deduction-based verification of workflow-oriented models is proposed. The process inference is based on the semantic tableaux method, which has some advantages when compared with traditional deduction strategies. The algorithm for automatic generation of logical specifications is proposed. The generation procedure is based on predefined workflow patterns for BPMN, which is a standard and dominant notation for the modeling of business processes. The main idea behind the approach is to consider patterns, defined in terms of temporal logic, as a kind of (logical) primitives which enable the transformation of models to temporal logic formulas constituting a logical specification. Automation of the generation process is crucial for bridging the gap between the intuitiveness of deductive reasoning and the difficulty of its practical application when logical specifications are built manually. This approach has gone some way towards supporting, hopefully enhancing, our understanding of deduction-based formal verification of workflow-oriented models.
3
Content available Weryfikowanie specyfikacji wymagań sterownika logicznego za pomocą diagramów aktywności UML, logiki temporalnej LTL i środowiska NuSMV
Grobelna I., Grobelny M.
Pomiary Automatyka Robotyka
|
2013
|
R. 17, nr 10
188--192
PL
W artykule przedstawiono ideę zastosowania diagramów aktywności UML do specyfikacji wymagań dotyczących zachowania sterownika logicznego. Lista wymagań podlegających weryfikacji zwykle definiowana jest bezpośrednio za pomocą formuł logiki temporalnej. Użycie przyjaznych dla użytkownika, powszechnie znanych i wykorzystywanych diagramów pozwala na prostsze i bardziej intuicyjne zapisanie wymagań. Diagramy są następnie formalnie przekształcane do formuł liniowej logiki temporalnej (LTL).
EN
The article introduces an idea to use UML activity diagrams [1-5] for specification of requirements regarding logic controller behavior. Requirements list to be verified [14] (using model checking technique [6, 7]) is usually directly defined using temporal logic formulas [12, 15]. Using user-friendly, commonly known and practiced diagrams allows to easier and more intuitively write down the requirements easier and more intuitively. Activity diagrams are then formally transformed into linear temporal logic (LTL) formulas. In this paper some sample UML activity diagrams which specify global properties are presented, together with their interpretation using LTL logic. To perform model checking process, model description (based i.e. on a control interpreted Petri net [8] or indirectly on an UML activity diagram [11]), and requirements list are needed. Afterwards it is checked, whether defined properties are satisfied in specified model description. If a requirement cannot be fulfilled, appropriate counterexample is generated allowing to localize error source. The article is structured as follows. Section 1 is an introduction. Background of a logic controller specification and its verification is presented in section 2. A novel approach to logic controller requirements definition using activity diagrams is shown in section 3. The paper ends with a short summary.
4
Content available From workflow design patterns to logical specifications
Klimek R.
Automatyka / Automatics
|
2013
|
Vol. 17, no. 1
59--63
EN
This work concerns issues related to automatic generation of logical specifications. Logical specifications can be extracted directly from developed software models. Received specification can be used in the process of a system formal verification using a deductive approach. The generated logical specification is just a set of temporal logie fonnulas as well as verified system properties are expressed in temporal logie. The extraction process is based on the idea of organizing the whole analyzed model as a set of certain design patterns of control flows. A method of automatic transformation of workflow design patterns to temporal logie formulas is proposed. These formulas constitute a logical specification and may be the first step towards a formal verification of system correctness using any method of the deduction-based reasoning. Applying the presented concepts enables bridging the gap between naturalness and intuitive of the deductive inference and the difficulty of its practical application in the case of software models.
PL
Praca dotyczy zagadnień związanych z automatyczną generacją i modelowaniem specyfikacji logicznej. Specyfikacja logiczna może być wygenerowana bezpośrednio z modeli oprogramowania. Tak uzyskana specyfikacja następnie może być wykorzystana w procesie formalnej weryfikacji przy wykorzystaniu podejścia dedukcyjnego. Wygenerowana specyfikacja reprezentowana jest przez zbiór formuł logiki temporalnej, również weryfikowane własności systemu mogą i powinny być wyrażone w logice temporalnej. Proces ekstrakcji opiera się na założeniu, aby cały analizowany model oprogramowania został zbudowany w oparciu o przyjęte, dowolne, ale najlepsze dla danej klasy zastosowań, wzorce projektowe. Została zaproponowana metoda automatycznej translacji wzorców projektowych (przepływów) do postaci formuł logiki temporalnej. Formuły te składają się na logiczną specyfikację i mogą stanowić pierwszy krok w kierunku formalnej weryfikacji poprawności systemów z wykorzystaniem dowolnej metody wnioskowania dedukcyjnego. Zastosowanie przedstawionych koncepcji umożliwia połączenie naturalności i intuicyjności samego wnioskowania logicznego oraz praktycznego zastosowania tych metod w przypadku modeli oprogramowania.
5
Formal analysis of destination reachability under given restrictions for multi-path routing in Network on Chip
Dziurzański P.
Elektronika : konstrukcje, technologie, zastosowania
|
2012
|
Vol. 53, nr 12
127-129
EN
In this paper, a technique for selecting proper restrictions in multi-path routing guarantying deadlock-freedom dedicated to Network on Chip (NoC) is presented. The proposed algorithm is based on the model checking utilizing computation tree temporal logic. This approach is illustrated with an example of features extraction module for the Automatic Speech Recognition (ASR) system. It is shown that even for this simple, 7-core MPSoC, selecting a wrong restriction may result in obtaining an unroutable on-chip network.
PL
W niniejszym artykule została przedstawiona technika wyboru odpowiednich ograniczeń wielościeżkowego routingu w sieciach wewnątrzukładowych, gwarantujących brak występowania blokad. Proponowany algorytm wykorzystuje sprawdzanie modeli z logiką temporalną drzew obliczeń CTL. Podejście zilustrowano przykładem ekstrakcji cech dla automatycznego rozpoznawania mowy. Pokazano, iż nawet dla tego prostego 7-rdzenowego układu typu MPSoC, wybór nieprawidłowego ograniczenia może skutkować uzyskaniem nierutowalnej sieci.
6
Content available remote Formal verification of embedded logic controller specification with computer deduction in temporal logic
Grobelna I.
Przegląd Elektrotechniczny
|
2011
|
R. 87, nr 12a
47-50
EN
The article presents a novel approach to formal verification of logic controller specification. Model checking technique is used to verify some behavioral properties. The approach proposes to use a rule-based logical model presented at RTL-level. Proposed logical model is suitable both for formal verification (model checking in the NuSMV tool) and for logical synthesis (using hardware description language VHDL). As the result, logic controller program (its implementation) will be valid according to its primary specification.
PL
Artykuł przedstawia nowatorskie podejście do formalnej weryfikacji specyfikacji sterownika logicznego. Zaproponowany został regułowy model logiczny, który jest dogodny zarówno do formalnej weryfikacji (weryfikacja modelowa w narzędziu NuSMV), jak również do syntezy logicznej (z użyciem języku opisu sprzętu VHDL). Program sterownika logicznego (jego implementacja) będzie zatem poprawny względem początkowej specyfikacji.
7
Content available Weryfikacja procesów biznesowych metodą dedukcyjną z wykorzystaniem logiki temporalnej
Klimek R.
Pomiary Automatyka Robotyka
|
2011
|
R. 15, nr 12
190-193
PL
Praca dotyczy formalnej analizy i weryfikacji modeli biznesowych wyrażonych w notacji BPMN. Weryfikacja oparta jest na wnioskowaniu dedukcyjnym. Jako metodę wnioskowania dla modeli biznesowych zaproponowano metodę tablic semantycznych, która cechuje się apagogicznością oraz analitycznością. Została przedstawiona metoda translacji podstawowych wzorców projektowych BPMN do formuł logiki temporalnej, stanowiących logiczną specyfikację analizowanegomodelu. Zarówno logiczna specyfikacja, jak i właściwości badanych procesów są wyrażone formułami tzw. najmniejszej logiki temporalnej. Formuły te są następnie przetwarzane z wykorzystaniem metody tablic semantycznych. Innowacyjność proponowanego podejścia może istotnie wpłynąć na redukcję kosztów wytwarzania oprogramowania, ze względu na możliwość wykrycia błędów oprogramowania już w fazie jego modelowania, wyprzedzając tym samym znacznie fazy implementacji i testowania.
EN
The paper concerns formal analysis and verification of business models expressed in BPMN. This verification is based on a deductive reasoning. As a method of inference for business models semantic tableaux method is proposed. Automatic trans- formations of the basic BPMN workflow patterns to temporal logic formulas are proposed. These formulas constitute a logical specification of the analyzed model. Both the logical specification and the desired system properties are expressed as formulas of the smallest linear temporal logic. These formulas are later processed using semantic tableaux method. Applying this innovative concept might result in software development costs reduction as some errors might be addressed in the modeling phase not in implementation or testing phase.
8
Content available Weryfikacja modelowa interpretowanych sieci Petriego sterowania
Grobelna I.
Pomiary Automatyka Kontrola
|
2011
|
R. 57, nr 6
666-670
PL
Artykuł przedstawia oryginalne podejście do weryfikacji modelowej interpretowanych sieci Petriego sterowania. Sieci Petriego są powszechnie wykorzystywane w przemyśle. Najczęściej jednak weryfikowane są pod kątem właściwości strukturalnych, a właściwości behawioralne (mimo ich dużego znaczenia) są pomijane. Technika weryfikacji modelowej pozwala na weryfikację właściwości opisujących zachowanie projektowanego systemu. Model logiczny otrzymany na podstawie istniejącej sieci Petriego sterowania przedstawiany jest na poziomie RTL w taki sposób, że nadaje się zarówno do formalnej weryfikacji, jak i do syntezy logicznej jako rekonfigurowalny sterownik logiczny lub PLC.
EN
The paper introduces a novel approach to model checking with Control Interpreted Petri Nets [15]. Petri Nets [9, 11, 12, 13] are commonly used in the industry. However, they are mostly verified against structural properties, and behavioral properties are out of scope. The model checking technique [3, 7, 8, 21, 22] allows verifying properties which describe behavior of the designed system. Properties to be verified are expressed in temporal logic [16, 17, 18, 19, 20]. The logical model (Fig. 1) derived from existing Petri net is presented at RTL level (Register Transfer Level) in such a way, that it is easy to be formally verified as well as to logical synthesized as a reconfigurable logic controller or PLC (Programmable Logic Controller). It operates on variables which correspond to places, input and output signals of the Control Interpreted Petri Net (Section 3). The variables change their values according to some specified rules. The logical model is afterwards transformed into input format of the NuSMV model checker [23] and formally verified (Section 4). Control Interpreted Petri Net (Fig. 2) is divided into elementary subnets (Fig. 3). Each elementary subnet consists of a single place and its input and output transitions. Each elementary subnet is interpreted as a single segment of model description in the NuSMV tool. Each elementary subnet represents a two-states state machine which is usually realized as a single macrocell (Fig. 4) in the FPGA circuit. The properties to be verified are expressed in LTL or CTL logic. If any of them is not satisfied in the described system model, the appropriate counterexample is generated (Fig. 6). In the example in the paper the verification finds a subtle error resulting from incorrect / incomplete specification (Fig. 5) and allows the user to localize the error source.
9
Content available remote First-Order Linear-time Epistemic Logic with Group Knowledge: An Axiomatisation of the Monodic Fragment
Belardinelli F., Lomuscio A.
Fundamenta Informaticae
|
2011
|
Vol. 106, nr 2-4
175-190
EN
We investigate quantified interpreted systems, a computationally grounded semantics for a first-order temporal epistemic logic on linear time. We report a completeness result for themonodic fragment of a language that includes LTL modalities as well as distributed and common knowledge. We exemplify possible uses of the formalismby analysingmessage passing systems, a typical framework for distributed systems, in a first-order setting.
10
Gaps in design and tests of dependable embedded systems
Grobelna I., Grobelny M.
Metody Informatyki Stosowanej
|
2010
|
nr 2 (23)
45-51
EN
The paper focuses on gaps in design and test technology for dependable embedded systems. Possible gaps in design may influence system behavior and as the result final product may not fulfill all requirements or some of desired properties. Test phase is also important as it may indicate even subtle errors which occurred in previous phases. The article presents possible solutions to improve the design and test technology. Model checking technique can be used for formal verification of specification in design phase. Testing phase can involve independent tester teams.
11
Content available Formal analysis of use case diagrams
Klimek R., Szwed P.
Computer Science
|
2010
|
Vol. 11
115-131
EN
Use case diagrams play an important role in modeling with UML. Careful modeling is crucial in obtaining a correct and efficient system architecture. The paper refers to the formal analysis of the use case diagrams. A formal model of use cases is proposed and its construction for typical relationships between use cases is described. Two methods of formal analysis and verification are presented. The first one based on a states' exploration represents a model checking approach. The second one refers to the symbolic reasoning using formal methods of temporal logic. Simple but representative example of the use case scenario verification is discussed.
PL
Diagramy przypadków użycia odgrywają znaczącą rolę w modelowaniu systemów z wykorzystaniem UML. Staranne i dokładne modelowanie ma zasadnicze znaczenie w postępowaniu umożliwiającym uzyskanie poprawnej i efektywnej architektury systemu. Artykuł odnosi się do formalnej analizy diagramów przypadków użycia. Został zaproponowany model formalny przypadku użycia, a także opisano odpowiednie konstrukcje dla relacji występujących pomiędzy przypadkami użycia. Zostały przedstawione dwie formalne metody ich analizy i weryfikacji. Pierwsza oparta jest na eksploracji stanów i reprezentuje podejście nazwane weryfikacją modelową. Druga odwołuje się do wnioskowania symbolicznego z wykorzystaniem logiki temporalnej. Został pokazany prosty i reprezentatywny przykład weryfikacji pewnego scenariusza przypadku użycia.
12
Content available Weryfikacja aktywności systemów modelowanych na bazie architektury SOA - prowadzona w oparciu o wymagania zadane diagramami przypadków użycia
Klimek R., Skrzyński P., Turek M.
Automatyka / Akademia Górniczo-Hutnicza im. Stanisława Staszica w Krakowie
|
2010
|
T. 14, z. 3/2
893-903
PL
Artykuł porusza zagadnienia formalnej weryfikacji wymagań dla tzw. systemów biznesowych, wyrażonych przez model przypadków użycia oraz scenariuszy przypadków użycia UML. Zaproponowana została metodologia opisująca przejście od diagramów przypadków użycia do diagramów aktywności. Do specyfikacji żądanych własności systemu została wykorzystana logika temporalna. Własności tak zakodowane mogą być następnie poddawane procesom weryfikacji z wykorzystaniem wnioskowania dedukcyjnego metodą tablic semantycznych. Zaproponowane zostały metody pozyskiwania formuł logiki temporalnej bezpośrednio ze scenariuszy przypadków użycia zapisanych w diagramach czynności UML.
EN
The article discusses the issue of f formal requirements verification for so-called "business systems" - expressed through an UML Use-Case model and Use-Case scenarios. A methodology for transformation of UML Use-Case diagrams to Activity diagrams has been described. To specify advanced system requirements a temporal logic notation was used. These requirements (encoded in such way) could be verified with a deductive inference based on semantic tables. The methods for obtaining temporal logic formulas directly from Use-Case scenarios stored in the UML Activity diagrams have also been introduced.
13
Content available Formalna weryfikacja maszyny stanów z wykorzystaniem logiki temporalnej
Grobelna I.
Pomiary Automatyka Kontrola
|
2009
|
R. 55, nr 7
457-460
PL
Artykuł przedstawia koncepcję specyfikacji współbieżnego procesu sterowania cyfrowego za pośrednictwem diagramów algorytmicznych maszyn stanów ASM w języku aprobowanym przez profesjonalne narzędzie model checker. Specyfikacja może zostać następnie formalnie zweryfikowana pod kątem wymagań stawianych projektowanemu systemowi. Lista wymagań tworzona jest przy wykorzystaniu liniowej logiki temporalnej LTL. Formalna weryfikacja Model Checking polega na sprawdzeniu, czy model systemu spełnia stawiane mu wymagania. W przypadku wykrycia niespóności generowany jest odpowiedni kontrprzykład.
EN
The paper presents the formal specification method of concurrent control processes in form of algorithmic state machines ASM [5] in a language accepted by a professional model checker tool NuSMV. Basing on linear temporal logic LTL [7, 8, 9, 16] a requirement list (Fig. 6) for the system model is prepared. Formal verification Model Checking [17, 19] consists in comparison of the model description and the requirements list. If some requirements cannot be fulfilled, the appropriate counterexample is generated (Fig. 7), which allows localizing the error source. The ASM diagrams (Fig. 4) are fully determined, but they do not support modularity, that is why they are not well suited for specification of concurrent controlling processes. The paper includes a short introduction to the theory of algorithmic state machines ASM (Section 2), temporal logic (Section 3) and model checking technique (Section 4). The proposed solution is presented on an example (Section 5) of the process of controlling (partially concurrent) movements of two vehicles (Fig. 2). The formal verification method of the ASM diagrams with its advantages and disadvantages as well as the general conclusions are given at the end of the paper (Section 6).
14
Formalna analiza interpretowanych algorytmicznych maszyn stanów ASM z wykorzystaniem narzędzia model checker
Grobelna I.
Metody Informatyki Stosowanej
|
2008
|
nr 3 (Tom 16)
107--124
EN
Algorithmic state machines ASM are one of formal methods of embedded systems specification. They are defined during system project phase. Potential not detected errors in specification may generate unnecessary costs, and in case of dependable systems they may even have catastrophic causes. The article presents formal verification and analysis method of algorithmic state machines using computer deduction in temporal logic (Model Checking technique). Model checker tools enable automatic verification of system specification by checking consistency between model description and requirements which have to be satisfied in the model. The paper concentrates on NuSMV model checker. Formal verification technique Model Checking is discussed basing on presented case study.
15
Content available remote Products of Tree Automata with an Application to Temporal Logic
Ésik Z., Iván S.
Fundamenta Informaticae
|
2008
|
Vol. 82, nr 1-2
61-78
EN
We introduce the notion of the Moore product of tree automata as a special case of the cascade product. We give an algebraic characterization of the expressive power of certain CTL-like temporal logics based on the notion of varieties of finite tree automata closed under the Moore product.
16
Content available remote Application of formal methods for hardware/software co-design of embedded systems
Piotrowicz M.
Zeszyty Naukowe. Elektryka / Politechnika Łódzka
|
2007
|
z. 111
89-94
EN
In the paper a new co-verification technique for mixed hardware/software systems has been presented. The presented solution has hierarchical coloured Petri nets implemented for modelling the system and also the temporal logie for describing any technical requirement of the controller. The presented technique has been verified on a practical design of DC motor pulse controller. Such an attempt should shorten the design phase and could be a very efficient tool for co-verification of the integrated design methodology.
PL
W pracy przedstawiono nową metodologię projektowania mieszanych sterowników wbudowanych. Propozycja autora zakłada wykorzystanie hierarchicznych kolorowanych sieci Petriego do modelowania artefaktów projektowanego systemu oraz logii temporalnej do formułowania wymaganych własności. Metoda ta została zweryfikowana na praktycznym przykładzie projektu sterownika impulsowego silnika prądu stałego.
17
Content available remote Uniform Satisfiability in PSPACE for Local Temporal Logics Over Mazurkiewicz Traces
Gastin P., Kuske D.
Fundamenta Informaticae
|
2007
|
Vol. 80, nr 1-3
169-197
EN
We study the complexity of temporal logics over concurrent systems that can be described by Mazurkiewicz traces. We develop a general method to prove that the uniform satisfiability problem of local temporal logics is in PSPACE. We also demonstrate that this method applies to all known local temporal logics.
18
Content available remote On First-Order Fragments for Mazurkiewicz Traces
Diekert V., Horsch M., Kufleitner M.
Fundamenta Informaticae
|
2007
|
Vol. 80, nr 1-3
1-29
EN
Mazurkiewicz traces form a model for concurrency. Temporal logic and first-order logic are important tools in order to deal with the abstract behavior of such systems. Since typical properties can be described by rather simple logical formulas one is interested in logical fragments. One focus of this paper is unary temporal logic and first-order logic in two variables. Over words, this corresponds to the variety of finite monoids called DA. However, over Mazurkiewicz traces it is crucial whether traces are given as dependence graphs or as partial orders (over words these notions coincide). The main technical contribution is a generalization of important characterizations of DA from words to dependence graphs, whereas the use of partial orders leads to strictly larger classes. As a consequence we can decide whether a first-order formula over dependence graphs is equivalent to a first-order formula in two variables. The corresponding result for partial orders is not known. This difference between dependence graphs and partial orders also affects the complexity of the satisfiability problems for the fragments under consideration: for first-order formulas in two variables we prove an NEXPTIME upper bound, whereas the corresponding problem for partial orders leads to EXPSPACE. Furthermore, we give several separation results for the alternation hierarchy for first-order logic. It turns out that even for those levels at which one can express the partial order relation in terms of dependence graphs, the fragments over partial orders have more expressive power.
19
Content available remote Decidability w.r.t. Logical Consecutions of Linear Temporal Logic Extended by Since and Previous
Rybakov V.V.
Fundamenta Informaticae
|
2007
|
Vol. 81, nr 1-3
297-313
EN
This paper aims to prove that the linear temporal logic LTLu,sn, n-1(N) , which is an extension of the standard linear temporal logic LTL by operations Since and Previous (LTL itself, as standard, uses only Until and Next) and is based on the frame of all natural numbers N, as generating Kripke/Hintikka structure, is decidable w.r.t. admissible consecutions (inference rules). We find an algorithm recognizing consecutions admissible in LTLu,sn, n-1(N) . As a consequence this algorithm solves satisfiability problem and shows that LTLu,sn, n-1(N) itself is decidable, despite LTLu,sn, n-1(N) does not have the finite model property.
20
Content available remote Expressing and Verifying Temporal and Structural Properties of Mobile Agents
Bednarczyk M.A., Jamroga W., Pawłowski W.
Fundamenta Informaticae
|
2006
|
Vol. 72, nr 1-3
51-63
EN
Logics for expressing properties of Petri hypernets, a visual formalism for modelling mobile agents, are proposed. Two classes of properties are of interest-the temporal evolution of agents and their structural correlation. In particular, we investigate how the classes can be combined into a logic capable of expressing the dynamic evolution of the structural correlation. The problem of model checking properties of a class of the logic on Petri hypernets is shown to be pspace-complete.
first rewind previous Strona / 2 next fast forward last
JavaScript jest wyłączony w Twojej przeglądarce internetowej. Włącz go, a następnie odśwież stronę, aby móc w pełni z niej korzystać.