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

Znaleziono wyników: 17

Liczba wyników na stronie
first rewind previous Strona / 1 next fast forward last
Wyniki wyszukiwania
help Sortuj według:

help Ogranicz wyniki do:
first rewind previous Strona / 1 next fast forward last
1
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.
2
Content available Weryfikacja modelowa hierarchicznej specyfikacji sterownika logicznego
Grobelna I., Grobelny M.
Pomiary Automatyka Kontrola
|
2013
|
R. 59, nr 8
796--798
PL
Specyfikacja zachowania projektowanego urządzenia powinna uwzględniać wszystkie elementy behawioralne. Z uwagi na złożoność projektowanych systemów szczególnie istotną rolę odgrywa możliwość dekompozycji. Z wykorzystaniem hierarchii można podzielić specyfikację na logiczne elementy połączone ze sobą na diagramach wyższego poziomu. W artykule przedstawiono zagadnienia związane z formalną weryfikacją hierarchicznych specyfikacji sterownika logicznego wyrażonych za pomocą interpretowanych sieci Petriego oraz diagramów aktywności języka UML.
EN
Specification of a designed logic controller should include all behavioral aspects. By complex systems design decomposition is especially valuable. Specification can be divided into parts using hierarchy. Logical elements are joined together at higher-level diagrams. The paper focuses on formal verification [1] of logic controller hierarchical specification by means of UML activity diagrams and interpreted Petri nets. Although hierarchy itself is presented in the considered specification techniques in different ways (complex activities by UML activity diagrams and macro-places/ macrotransitions by Petri nets), it is possible to use both techniques together in one project and to transform anytime one diagram into the another [5, 9, 10] (example in Figs. 1 and 2). In the transformation process, UML activity diagram actions correspond to Petri net transitions [7, 8]. Model checking [2, 3] of hierarchical specification can be performed step by step, e.g. by means of the NuSMV tool [11]. Rule-based specification (based on a Petri net) can be checked against behavioral properties [12, 13] expressed by temporal logic formulas [4]. Macroplaces can be verified separately (Fig. 3 considering local properties) and/or concurrently (Fig. 4, Fig. 5 considering mutual correlation and global properties). Next, the whole Petri net with macroplaces can be checked (Fig. 6). Sometimes it is convenient to verify a complete net (not hierarchical), like in [14]. Formal verification of specification can significantly increase its quality, and the support for hierarchy simplifies complex systems verification.
3
Regułowy model logiczny rekonfigurowalnego sterownika logicznego do weryfikacji i syntezy
Grobelna I.
Studia Informatica
|
2012
|
Vol. 33, nr 1
59-75
PL
Artykuł przedstawia regułowy model logiczny rekonfigurowalnego sterownika logicznego opisanego za pomocą interpretowanej sieci Petriego, która jest formalną specyfikacją zachowania systemów dyskretnych. Model logiczny, jako abstrakcyjny opis, nadaje się zarówno do formalnej weryfikacji, jak i syntezy logicznej. W pracy są rozpatrywane różne warianty opisu reguł.
EN
The article presents rule-based logical model of reconfigurable logic controller, by means of Control Interpreted Petri Nets, which are formal specification of discrete systems behavior. Logical model, as an abstract description, is easy to formally verify and to synthesize. In the paper, various rules notations are discussed.
4
Content available Projektowanie sterowników logicznych z wykorzystaniem łuków zezwalających i zakazujących sieci Petriego
Grobelna I., Grobelny M.
Pomiary Automatyka Kontrola
|
2012
|
R. 58, nr 7
605-607
PL
Artykuł dotyczy zagadnień związanych z projektowaniem sterowników logicznych z wykorzystaniem łuków zezwalających i zakazujących sieci Petriego. Zaproponowano nowatorskie podejście do regułowej specyfikacji sterownika logicznego, przygotowanej w postaci abstrakcyjnego autorskiego modelu logicznego dogodnego do formalnej weryfikacji modelowej oraz syntezy logicznej. Szczególną uwagę zwrócono tutaj na łuki zakazujące i zezwalające interpretowanych sieci Petriego, ich realizację w abstrakcyjnym modelu logicznym i interpretację w innej postaci specyfikacji zachowania sterownika logicznego - diagramach aktywności języka UML.
EN
The paper focuses on logic controller design using enabling and inhibitor arcs of Petri nets. There is proposed a novel original approach to rule-based specification of logic controller behaviour prepared as an abstract logical model suitable for formal verification and logic synthesis. Special interest is put on enabling and inhibitor (disabling) arcs of interpreted Petri nets, their realization in an abstract logical model and interpretation in other specification form - namely UML activity diagrams (in version 2.x). These arcs can be used for flow synchronization or controlled usage of shared resources. After a short introduction (Section 1), some basic concepts on logic controller specification are presented (Section 2), in particular considering (interpreted) Petri nets and UML (activity) diagrams. Usage of enabling and inhibitor arcs is shown on an example of the interpreted Petri net in Fig. 1 (transitions firing sequence in Fig. 2), followed by their representation in the proposed abstract rule-based logical model, its formal verification (using model checking technique) and synthesis (Section 3). The paper also proposes enabling and inhibitor arcs interpretation in UML activity diagrams (Section 4). Although direct representation of these arcs is not possible, the authors try to achieve an alternative solution which corresponds semantically to appropriate Petri net elements. Tab. 1 presents graphic representation of the considered arcs in interpreted Petri nets as well as in UML activity diagrams. The paper ends with a short summary (Section 5).
5
Content available Inhibitor and enabling arcs in logic controller design
Grobelna I., Grobelny M.
Pomiary Automatyka Kontrola
|
2012
|
R. 58, nr 6
510-513
EN
The paper presents a novel approach to rule-based logic controller specification and its verification. The proposed abstract model is suited for formal verification (using model checking technique) as well as for logic synthesis (using hardware description language VHDL). Special focus is put on Interpreted Petri Nets with inhibitor and enabling arcs, their realization in rule-based model and, additionally, their interpretation in another logic controller specification technique - UML Activity Diagrams (version 2.x).
PL
Artykuł przedstawia nowatorskie podejście do regułowej specyfikacji sterownika logicznego, wraz z jej weryfikacją (walidacją). Proponowany abstrakcyjny model logiczny jest dogodny zarówno do formalnej weryfikacji modelowej, jak również do syntezy logicznej (język opisu sprzętu VHDL). Szczególną uwagę poświęcono łukom zakazującym i zezwalającym interpretowanych sieci Petriego. Po krótkim wprowadzeniu do omawianej tematyki (rozdział 2), przedstawiono przykład interpretowanej sieci Petriego z łukami zakazującymi i zezwalającymi (rys. 1). Podano sposób ich realizacji w abstrakcyjnym modelu logicznym (rozdział 3, schemat kompletnego proponowanego systemu na rys. 2 oraz przykład regułowego modelu sterownika logicznego na rys. 3). Zaproponowano interpretację łuków zakazujących i zezwalających sieci Petriego w innej postaci specyfikacji zachowania sterownika logicznego (rozdział 4) - diagramach aktywności języka UML (w wersji 2.x). Ze względu na bezstanowość diagramów aktywności, nie jest możliwe bezpośrednie odwzorowanie rozpatrywanych łuków. W artykule zaproponowano dwa rozwiązania - opierające się na wprowadzeniu dodatkowego sygnału (rys. 4a) oraz alternatywne - bazujące na etykietowaniu przepływów (rys. 4b). Przedstawiono sposób formalnej weryfikacji tak przygotowanej specyfikacji regułowej oraz jej syntezy logicznej (rozdział 5). Publikacja kończy się podsumowaniem oraz wnioskami (rozdział 6)
6
Content available Diagramy aktywności UML w projektowaniu rekonfigurowalnych sterowników logicznych
Grobelny M., Grobelna I.
Pomiary Automatyka Kontrola
|
2012
|
R. 58, nr 7
596-598
PL
Artykuł przedstawia sposób reprezentacji behawioralnej sterownika logicznego przy wykorzystaniu diagramów aktywności języka UML. Zaproponowane zostało zastosowanie diagramów aktywności do projektowania rekonfigurowalnych sterowników logicznych, a dokładnie do opisu zachowania sterownika logicznego podczas pracy. Do tego celu został dostosowany zbiór elementów diagramów aktywności w celu umożliwienia efektywnego modelowania behawioralnego. Rozważane jest także wykorzystanie hierarchicznych możliwości diagramów aktywności do częściowej rekonfiguracji
EN
The paper focuses on behavioural representation of a logic controller with usage of UML activity diagrams. There is shown a subset of UML activity diagram elements sufficient to present logic controller behaviour simultaneously suitable for automatic synthesis with use of hardware description languages. After short introduction (Section 1) to the topic, UML activity diagrams as a specification technique are presented (Section 2). Additionally, there is described a subset of elements (Tab.1) of the discussed specification techniques fulfilling behavioural modelling requirements of a reconfigurable logic controller. Specification possibilities are given using sample control process of preparing the exact amount of liquid in two tanks (Section 3). The real model of the process is shown in Fig. 1. One of the possible behavioural specifications with use of UML activity diagrams is depicted in Fig. 2. This is a representation of the considered action state concept specification techniques in version 1.x. The other possibility is to specify a process with use of elementary system actions (Fig. 3), which is characteristic of the UML activity diagrams version 2.x. Fig. 4, on the other hand, shows signal based specification which is suitable for automatic hardware description language code generation (e.g. VHDL). Furthermore, Section 4 describes possibilities of using hierarchical aspects of activity diagrams to prepare specification for partial reconfiguration. Finally, Section 5 concludes the paper.
7
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.
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 Regułowa reprezentacja interpretowanych sieci Petriego sterowania dla potrzeb syntezy i weryfikacji
Grobelna I.
Pomiary Automatyka Kontrola
|
2011
|
R. 57, nr 8
942-944
PL
Artykuł proponuje regułowy sposób reprezentacji interpretowanych sieci Petriego sterowania w logice temporalnej. Sposób ten jest przydatny zarówno do formalnej weryfikacji modelowej, jak i do automatycznej syntezy logicznej z wykorzystaniem języków opisu sprzętu (Verilog, VHDL) jako rekonfigurowalny sterownik logiczny lub PLC. Sieci Petriego weryfikowane są zwykle tylko pod kątem właściwości strukturalnych. Technika weryfikacji modelowej pozwala na weryfikację właściwości behawioralnych opisujących zachowanie projektowanego systemu.
EN
The paper presents a novel idea of Control Interpreted Petri Nets representation in temporal logic. The proposed logic representation is suitable both for formal model checking and automatic synthesis using hardware description languages (Verilog, VHDL). Petri Nets [1, 2, 3] are currently used in industry, i.e. by logic controller design [4]. Dedicated tools for creating Petri Nets support verification against structural properties. Behavioral properties are also of great importance, however they are rarely considered. Model checking technique [5] allows for verification of properties describing behavior of designed system. So far, there have been some approaches to verify (validate) specification by means of Petri Nets [6, 7, 8, 9], by means of UML diagrams [10] or logic controller programs in ST language [11]. However, none of them have addressed Control Interpreted Petri Nets focused on RTL level. The proposed rule-based representation of Control Interpreted Petri Nets (logical model in Figs. 2-5) is easy to formally verify (model description for NuSMV model checker [13] in Fig. 6-10), as well as to synthezise (VHDL model in Figs. 11-13) as a reconfigurable logic controller or PLC. Verified behavioral specification in temporal logic [14] is an abstract program of matrix reconfigurable logic controller functionality, and logic controller program (implementation) satisfies its primary specification. The logical model built from Control Inter-preted Petri Net describes it in a strict and short form.
10
Content available Problem hierarchii w transformacji diagramów aktywności UML 2.x do sieci Petriego sterowania
Grobelny M., Grobelna I.
Pomiary Automatyka Kontrola
|
2011
|
R. 57, nr 7
729-732
PL
Proces specyfikacji zachowania odgrywa istotną rolę z powodu określania na tym etapie cech i sposobu funkcjonowania sterownika logicznego. W artykule omówione zostały dwie metody graficznego specyfikowania zachowania sterowników logicznych - diagramy aktywności języka UML 2.x oraz sieci Petriego sterowania. Zaproponowana została metoda transformacji hierarchicznych diagramów aktywności do hierarchicznych sieci Petriego. Dzięki przedstawionej metodzie możliwe jest połączenie zalet obu typów graficznego opisu specyfikacji urządzeń. Dodatkowo, zaproponowana została metoda formalnej weryfikacji hierarchicznej formy specyfikacji umożliwiająca wykrycie potencjalnych błędów na tym wczesnym etapie projektu.
EN
Behavior specification is one of the most important steps in embedded systems design. It plays a significant role because system properties and functionality are specified in this phase. There exist some techniques which can be helpful for a designer. In the paper two methods for graphical specification of logic controller behavioral specification [1, 2, 6], namely UML 2.x activity diagrams [10] and control Petri nets [11], are considered. A novel transformation method for transformation of hierarchical activity diagrams into hierarchical Petri nets is proposed. The presented method allows combining the advantages of both types of graphical system specification. Additionally, a formal verification method for hierarchical specification form is proposed. It enables detecting potential errors at early stage of system development. Hierarchical form of specification is commonly used in design process. Activity diagrams can include complex actions (Fig. 1) which describe some subprocesses. Petri nets also support hierarchy, but it can be realized in two different forms [9] - as macroplaces or macrotransitions (Fig. 2). According to the transformation method from [3, 8], actions in activity diagrams are interpreted as transitions in Petri net. In hierarchical processes by means of Petri nets two elements, macrotransitions (Fig. 3) and macroplaces (Fig. 4), have to be considered. The macroplace (Fig. 5a) can be surrounded by two transitions (Fig. 5b), decomposed (Fig. 5c), and finally compressed to macrotransition (Fig. 5d), then transformed into complex activity in an UML 2.x activity diagram (Fig. 5e). Verification of both considered specification forms [3] allows comparing two versions of the same behavior description. The model checking technique [4] can be used to verify the whole system or a part of it. Partial verification can be used for hierarchical specifications, as the verification process can be performed step by step (Fig. 6).
11
Wprowadzenie do weryfikacji i symulacji w środowisku NuSMV
Grobelna I.
Metody Informatyki Stosowanej
|
2011
|
nr 1
23-30
PL
Specyfikacja systemu informatycznego jest jednym z pierwszych etapów jego tworzenia i stanowi fundament dalszych prac. Na tym etapie projektu określany jest sposób działania systemu oraz właściwości jego pracy. Należy zadbać o to, aby specyfikacja była w pełni poprawna, a zaprojektowany system spełniał wszystkie stawiane mu wymagania . Jedną z metod walidacji specyfikacji jest weryfikacja oraz symulacja modelu systemu. Oba zadania mogą zostać wykonane w środowisku NuSMV.
EN
The article is a short introduction into model checking and simulation in the NuSMV environment. The NuSMV tool allows description offinite state machines FSM and their verification using temporal logic formulas. Using a simple example (traffic lights), basic rules and commands of model checking and simulation process are presented. Using the NuSMV environment it is possible to detect some errors at an early stage of system development.
12
Automatyczna weryfikacja i synteza regułowego modelu sterownika logicznego
Grobelna I.
Metody Informatyki Stosowanej
|
2011
|
nr 3
59-65
EN
The article focuses on model checking and synthesis of rule-based specification of logic controller. It describes and illustrates proposed design system of logic controllers. Specification by means of Control Interpreted Petri Nets is formally written as rule-based logical model, which is suitable both for formal verification against behavioral requirements and for synthesis in form of reconfigurable logic controller. Verifiable model is thereby consistent with synthesizable model. Logical model is also used for behavioral verification and simulation. Translation process of rule-based specification into verifiable model description and synthesizable code has been automated.
13
Content available Petri nets and activity diagrams in logic controller specification – transformation and verification
Grobelna I., Grobelny M., Adamski M.
Zeszyty Naukowe. Telekomunikacja i Elektronika / Uniwersytet Technologiczno-Przyrodniczy w Bydgoszczy
|
2010
|
z. 13
79--91
EN
The paper presents formal verification method of logic controller specification taking into account user-specified properties. Logic controller specification may be expressed as Petri net or UML 2.0 Activity Diagram. Activity Diagrams seem to be more user-friendly and easy-understanding that Petri nets. Specification in form of activity diagram may afterwards be transformed into Petri net, which may then be formally verified and used to automatically generate implementation (code). A new transformation method dedicated for event-driven systems is proposed. Verification process is executed automatically by the NuSMV model checker tool. Model description based on specification and properties list is being built. Model description derived from Petri net is presented in RTL-level and easy to synthesize as reconfigurable logic controller or PLC. Properties are defined using temporal logic. In model checking process, verification tool checks whether requirements are satisfied in attached system model. If this is not the case, appropriate counterexamples are generated.
PL
Praca prezentuje metodę formalnej weryfikacji specyfikacji sterownika logicznego uwzględniającą właściwości podane przez użytkownika. Specyfikacja sterownika logicznego może być przedstawiona m.in. w postaci sieci Petriego lub diagramu aktywności języka UML. Diagramy aktywności wydają się być bardziej przyjazne i zrozumiałe dla użytkownika niż sieci Petriego. Specyfikacja w postaci diagramu aktywności może zostać przekształcona do sieci Petriego, która następnie może być formalnie zweryfikowana i wykorzystana do automatycznej generacji implementacji (kodu). Węzły diagramu aktywności konsekwentnie interpretowane są jako tranzycje sieci Petriego, w odróżnieniu od klasycznego podejścia (w starszych wersjach UML) gdzie odwzorowywało się je jako miejsca sieci Petriego. Proces weryfikacji wykonywany jest automatycznie przez narzędzia weryfikacji modelowej. Tworzony jest opis modelu bazujący na specyfikacji oraz lista wymagań. Nowatorskim podejściem jest przedstawienie sieci Petriego na poziomie RTL w taki sposób, że łatwo jest przeprowadzić syntezę logiczną sieci w postaci współbieżnego rekonfigurowalnego sterownika logicznego lub sterownika PLC bez konieczności przekształcania modelu. Wymagania określone są przy użyciu logiki temporalnej. W procesie weryfikacji modelowej narzędzie weryfikujące NuSMV sprawdza, czy model systemu spełnia stawiane mu wymagania. Jeżeli tak nie jest, generowany jest odpowiedni kontrprzykład.
14
Content available Diagramy aktywności języka UML i sieci Petriego w systemach sterowania binarnego - od transformacji do weryfikacji
Grobelny M., Grobelna I.
Pomiary Automatyka Kontrola
|
2010
|
R. 56, nr 10
1154-1158
PL
Język UML jest technologią powszechnie stosowaną w świecie naukowym oraz w przemyśle. Sieci Petriego są modelem matematycznym ogólnego zastosowania ugruntowanym od wielu lat. Obie te techniki doskonale nadają się do specyfikacji procesów sterowania. Jednakże jako odmienne, każda z nich posiada unikatowe właściwości. Technika weryfikacji modelowej jest jedną z metod formalnej weryfikacji specyfikacji pozwalającą na zdiagnozowanie błędów w specyfikacji wymagań albo w opisie modelu. Artykuł przedstawia metodę transformacji pomiędzy obiema wymienionymi technikami specyfikacji w celu formalnej weryfikacji projektu sterowania opisanego w języku UML.
EN
Unified Modeling Language (UML) [1-3, 5, 6-8] is commonly used in scientific and industrial world. Petri nets [9] are mathematical model used for a long period of time. Both techniques are well suited for control processes specification. However, they are quite different. Each technique has its own unique properties. Model checking technique [14-17] is one of formal verification methods [18] for specifications. It allows detecting errors either in requirements specification or in model description. The paper presents the method for transformation between both mentioned specification techniques - from UML activity diagram (Fig. 1) to Petri net (Fig. 4), using some defined rules [10, 11]. Mapping of particular elements is presented in Table 1. Petri net after direct transformation may include redundant places which can be after-wards removed. Then, it is possible to formally verify control process described in UML. The proposed model checker tool is NuSMV [20]. NuSMV (Fig. 5) compares model description (Fig. 6 - 8) and requirements (Fig. 9) which have to be fulfilled. The requirements are defined using temporal logic. If a specified requirement may not be fulfilled, appropriate counterexamples are generated (Fig. 10) which allow detecting an error source. Then, the specification can be corrected and model checking process can start again, sometimes including only the particular part of a designed system.
15
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.
16
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).
17
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.
first rewind previous Strona / 1 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ć.