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

Znaleziono wyników: 13

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

help Ogranicz wyniki do:
first rewind previous Strona / 1 next fast forward last
1
Content available remote Towards energy-aware cyber-physical systems verification and optimization
Soltani Reza, Kang Eun-Young, Heredia Mena Juan Esteban
Annals of Computer Science and Information Systems
|
2021
|
Vol. 26
205--210
EN
Optimizing CPS behavior in terms of energy consumption can have a significant impact on system reliability. The environment influences the system's behavior, and neglecting the environmental behavior has indirect negative impact on optimizing the system's behavior. In this work, to increase the system's flexibility, the behavior of the environment is modeled dynamically to apply the disorderliness of its behavior. The resulting models are formally verified. By examining the past environmental behavior and predicting its future behavior, energy optimization is done more dynamically. The verification results acquired using a UPPAAL-SMC show that the optimization of system behavior by predicting the environmental behavior has been successful. Our approach is demonstrated using a case study within an I4 setting.
2
Content available remote Modeling and Verification using Different Notations for CPSs: The One-Water-Tank Case Study
Staroletov Sergey, Schulte Horst, Baar Thomas, Konyukhov Ivan, Shilov Nikolay, Rozov Andrei, Liakh Tatiana, Zyubin Vladimir
Annals of Computer Science and Information Systems
|
2021
|
Vol. 25
485--488
EN
The choice of an adequate notation and subsequent system formalization are the crucial points for the design of cyber-physical systems (CPSs). Here, an appropriate notation allows an explicit specification of the deterministic system behavior for specified initial states and inputs. We base our study on an industrial example (water tank) that comprises nominal as well as safety-critical states, and focus on the notation’s support to validate/verify crucial safety properties. Several industrial notations (e.g. Matlab/Simulink©) to design and simulate such a hybrid system have been tried based on our physical model. In addition, we remodel our example using the well-founded mathematical formalism of hybrid automata. It enables us to formally express and verify important safety properties using the theorem prover KeYmaera
3
Content available remote Towards Extending UML's Activity Diagram for the Architectural Modeling, Analysis, and Implementation
Kose Mehmet Alp, Ozkaya Mert
Annals of Computer Science and Information Systems
|
2020
|
Vol. 21
639--648
EN
SAWUML is a general-purpose software modeling language that extends UML by unifying component and sequence diagrams for the specifications of software architectures. While component diagram is used for modeling the system structures, sequence diagram is extended with the Design-by-Contract approach for the modeling of system behaviors. In this paper, we aim at enhancing the language usability by providing alternative modeling choices for practitioners. To this end, we extended SAWUML's notation set with UML's activity diagram for the behavior modeling. So, practitioners may now use either sequence or activity diagrams, while the system structures are still modeled with component diagrams. We also extended SAWUML's modeling editor for creating software architecture models together with component and activity diagrams and the code generators for automatically obtaining (i) formal models in SPIN's ProMeLa for formal verification and (ii) Java-based implementation. We illustrate our language extension with the gas station case-study.
4
Content available remote Requirement Elicitation Techniques for Software Projects in Ukrainian IT: An Exploratory Study
Gobov Denys, Huchenko Inna
Annals of Computer Science and Information Systems
|
2020
|
Vol. 21
673--681
EN
Elicitation is a core business analysis/requirements engineering activity that provides inputs for others like analysis, specification, confirmation, management. There is a significant number of specialized techniques that are used for requirement elicitation. The selection of the appropriate techniques considerably influences a project plan and success of a change as a whole. This paper is intended to analyze the industrial standards and experience of business analysts and requirement engineers in the part of elicitation activities. We conducted a survey study involving 328 specialists from Ukrainian IT companies and a series of interviews with experts to interpret the survey results. Furthermore, this paper provides the guideline in selecting a particular elicitation technique with respect to the type of project and situation.
5
Content available An automatic formal verification tool for schematic-level design of an electrical project
Szelest M.
Pomiary Automatyka Kontrola
|
2014
|
R. 60, nr 6
369--372
EN
Schemat ideowy układu elektronicznego może być postrzegany jako zbiór wzajemnie połączonych komponentów elektronicznych tworzących pewien graf połączeń. Graf ten jest strukturą, której topologia może być odczytana i przeanalizowana. Automatyczna weryfikacja formalna schematu ideowego ma na celu wykrycie nietrywialnych błędów (związanych ze strukturą tegoż schematu), popełnionych przez projektanta w trakcie opracowywania schematu. Błędy te są efektem pominięcia lub niewłaściwego wykorzystania elementów elektronicznych w typowych podukładach (blokach funkcjonalnych). W artykule opisano realizację komputerowego narzędzia wspomagającego proces automatycznej weryfikacji formalnej, począwszy od określenia sposobu zapisu schematu, przez integrację z komercyjnymi narzędziami EDA (ang. Electronic Design Automation) aż po określenie algorytmów identyfikujących podobwody. Opracowane narzędzie umożliwia dokonanie weryfikacji schematu ideowego już w bardzo wczesnych etapach procesu projektowego, co znacząco redukuje liczbę pętli w procesie projektowym, wpływając korzystnie na końcowy koszt opracowania produktu oraz skracając czas niezbędny do przygotowania urządzenia do produkcji.
PL
A schematic diagram can be interpreted as set of components connected together to build a network. The network is a structure whose topology can be read and analyzed. The automatic formal verification aims at detecting some non-trivial mistakes, made by an electrical engineer, connected with the structure of schematic, building blocks and typical functional sub circuits. The paper presents the approach for realization of an automatic formal detection tool starting from the definition of schematic structure, through connectivity with a schematic-capture tool, to a sub-circuit identification algorithm.
6
Content available Selection of search strategies for solving 3-SAT problems
Pułka A.
International Journal of Applied Mathematics and Computer Science
|
2014
|
Vol. 24, no. 2
283--297
EN
The paper concerns the problem of Boolean satisfiability checking, which is recognized as one of the most important issues in the field of modern digital electronic system verification and design. The paper analyzes different strategies and scenarios of the proving process, and presents a modified and extended version of the author’s FUDASAT algorithm. The original FUDASAT methodology is an intuitive approach that employs a commonsense reasoning methodology. The main objective of the work is to investigate the SAT-solving process and try to formulate a set of rules controlling the reasoning process of the FUDASAT inference engine. In comparison with the author’s previous works, the paper introduces new mechanisms: hypergraph analysis, multiple variable assignments and search space pruning algorithms. The approach considers only 3-SAT class functions, although a generalization of the method is discussed as well. The presented approach has been tested on various benchmarks and compared with the original pure FUDASAT algorithm as well as with other algorithms known from the literature. Finally, the benefits of the proposed SAT solving technique are summarized.
7
Automatyczna weryfikacja formalna układu elektronicznego w oparciu o schemat ideowy
Szelest M., Izydorczyk J., Niemiec H., Jabłeka M.
Elektronika : konstrukcje, technologie, zastosowania
|
2013
|
Vol. 54, nr 8
111-114
PL
Schemat ideowy układu elektronicznego jest zbiorem wzajemnie ze sobą połączonych elementów elektronicznych tworzących pewną sieć. Sieć ta jest strukturą, która może być w automatyczny sposób odczytywana analizowana. Automatyczna weryfikacja formalna schematu ideowego ma na celu wykrycie nietrywialnych błędów popełnionych przez projektanta w trakcie opracowywania schematu ideowego. W ramach analizy sprawdzana jest poprawność struktury i zgodność wartości wybranych parametrów tworzonego schematu w odniesieniu do - zdefiniowanych wcześniej - typowych bloków funkcyjnych. W artykule przestawiono przykładową realizację automatycznej weryfikacji formalnej przeprowadzaną w celu dokonania analizy klucza tranzystorowego począwszy od definicji okładu klucza tranzystorowego, przez sposób dostępu do schematu, po automatyczną identyfikację bloków funkcyjnych.
EN
Schematic diagram can be interpreted as set of components connected with themselves together to build a network. The network is a structure, which topology that can be red and analyzed. Automatic formal verification aims to detect some non-trivial mistakes, made by electrical engineer, connected with structure of a schematic, building blocks and typical functional sub-circuits. The article presents approach to realize automatic formal detection tool starting from definition of schematic structure, though connectivity with schematic-capture tool, to sub-circuit identification algorithm.
8
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.
9
An effective SAT-Solving mechanism with backtrack controlled by FDL
Pułka A.
Elektronika : konstrukcje, technologie, zastosowania
|
2011
|
Vol. 52, nr 12
21-25
EN
This work presents a novel approach to SAT solving problem based on commonsense reasoning methodology. The methodology has been implemented and tested in PROLOG. Discussion of different modern approaches to the satisfiability that have been published recently is presented. A parallelism between the SAT solving problem and non-monotonic extensions verifying is given. The new algorithm of SAT solving based on fuzzy default reasoning (FDL) theory FUDASAT and cumulativity of CNF formulas is defined. Optimal backtracking search methodology is explained on examples. Some experiments on various benchmarks show the efficiency and advantages of the proposed methodology.
PL
Artykuł przedstawia nowe podejście do problemu badania spełnialności formuł logicznych oparte na metodzie wnioskowania zdroworozsądkowego. Zaproponowana metoda została zaimplementowana i przetestowana w środowisku języka PROLOG. Przeprowadzono szczegółową dyskusję dotyczącą istniejących nowoczesnych technik sprawdzania spełnialności formuł logicznych, które zostały opublikowane w ostatnich latach. Przedstawiono podobieństwa między problemem badania spełnialności formuł logicznych a weryfikacją rozszerzeń w logice niemonotonicznej. Sformułowano podstawowe założenia nowego algorytmu FUDASAT badania spełnialności formuł logicznych opartego na wnioskowaniu FDL oraz zdefiniowano problem kumulacyjności formuł w postaci normalnej CNF. Metoda optymalnego przeszukiwania podczas nawrotów została opisana na przykładach. Eksperymenty przeprowadzone na zestawach wzorcowych pokazują zalety proponowanej metody.
10
Strategia weryfikacji systemu na chipie oparta na mechaniźmie FDL
Pułka A.
Elektronika : konstrukcje, technologie, zastosowania
|
2010
|
Vol. 51, nr 12
87-90
PL
Artykuł dotyczy zagadnień weryfikacji formalnej złożonych systemów elektronicznych, tzw. SoC. W pracy zaproponowano nowe oryginalne podejście do planowania strategi weryfikacji opartej o wnioskowanie zdroworozsądkowe. Opisano formalną metodologię mechanizmu planowania bazującą na rozproszonej logice domniemań FDL (Fuzzy Default Logic). Zdefiniowano wieloetapową strategię weryfikacji w postaci narzędzia systemu weryfikacji związanej z określoną platformą sprzętowo-programową. Metodologia została zweryfikowana na prototypowej platformie SoC połączonej magistralą AMBA. Pokazano zalety proponowanego podejścia.
EN
The paper deals with problem of the formal verification of complex electronic embedded systems. A new commonsense strategy is proposed. The formal methodology of the inference engine modeling based on Fuzzy Default Logic is given. The multistage verification strategy as the platform dependent verification (PDV) toolset is defined. The methodology has been validated on examples on a prototype AMBA-based virtual SoC platform working with SystemVerilog verification procedures. The advantages of the presented methodology have been emphasized.
11
Content available remote Analysis and design of correct real-time safety-critical software
Kosęda B.
Zeszyty Naukowe. Elektryka / Politechnika Łódzka
|
2008
|
z. 115
59-67
EN
High-energy physics experiments rely on large hardware installations. As these machines become more and more advanced, their maintenance becomes a complex task. The free-electron laser FLASH is not an exception. It is designed for delivering a high quality laser beam to scientific experiments round the clock. Each machine standstill costs extra money. Therefore, the maximization of its uptime plays an important role. Automation software is a means for improving machine availability. One expects to improve the machine uptime by automating routine tasks performed by the operators and by providing auto-recovery supervision software. The efforts presented in this contribution concern the elaboration of a general framework for the design and development of safe and predictable automation software. Devised tools and design methods are evaluated during the implementation of the automation software for a single RF-power station of the FLASH.
PL
Eksperymenty fizyki wysokich energii są możliwe dzięki zastosowaniu skomplikowanych instalacji eksperymentalnych. Z roku na rok urządzenia te stają się coraz bardziej skomplikowane a ich obsługa oraz serwisowanie staje się coraz bardziej złożona. Laser na elektronach swobodnych FLASH nie jest wyjątkiem. Jest to skomplikowane 260-metrowe urządzenie wykorzystujące najnowsze rozwiązania technologiczne. Laser ten produkuje wysokiej jakości wiązkę laserową. Ponieważ FLASH jest projektem komercyjnym, każdy zastój urządzenia wiąże się ze stratami finansowymi, Zadaniem oprogramowania nadzorującego pracę podsystemów akceleratora jest wydłużenie czasu jego poprawnej pracy. Zakłada się, że ten cel może być osiągnięty za pomocą automatyzacji rutynowych zadań wykonywanych przez operatorów oraz opracowania oprogramowania usuwającego symptomy drobnych awarii. Zagadnienia poruszane w artykule dotyczą opracowania metodyki i zestawu narzędzi do projektowania i implementacji oprogramowania automatyzującego. Prezentowane podejście i narzędzia omawiane są w kontekście systemu automatyzacji pojedynczej stacji zasilania lasera FLASH.
12
Content available Reprezentacja przestrzeni stanów sterownika logicznego z wykorzystaniem kodowanych diagramów decyzyjnych
Bubacz P., Adamski M.
Pomiary Automatyka Kontrola
|
2007
|
R. 53, nr 5
24-26
PL
W pracy porównano znane z literatury metody zwartej reprezentacji przestrzeni stanów dla rekonfigurowanego sterownika logicznego. Przedstawiono zalety heurystycznego sposobu kodowania miejsc sieci Petriego, dzięki któremu uzyskuje się diagramy OBDD o znacznie mniejszej złożoności przydatne zarówno podczas analizy, jak i syntezy układowej algorytmu sterowania binarnego.
EN
In the paper some known methods for an effective representation of the state space in reconfigurable logic controller are compared. The advantages of heuristic method of Petri net place encoding, which is adapted for a compact encoding technique of Binary Decision Diagrams, are given.
13
Content available remote FSM encoding for BDD representations
Gosti W., Villa T., Saldanha A., Sangiovanni-Vincentelli A. L.
International Journal of Applied Mathematics and Computer Science
|
2007
|
Vol. 17, no 1
113-128
EN
We address the problem of encoding the state variables of a finite state machine such that the BDD representing the next state function and the output function has the minimum number of nodes. We present an exact algorithm to solve this problem when only the present state variables are encoded. We provide results on MCNC benchmark circuits.
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ć.