PL
 |
EN
Nowa wersja platformy, zawierająca wyłącznie zasoby pełnotekstowe, jest już dostępna.
Przejdź na https://bibliotekanauki.pl
Preferencje help
Polish version English version Język
Widoczny [Schowaj] Abstrakt
Liczba wyników

Znaleziono wyników: 10

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

help Ogranicz wyniki do:
first rewind previous Strona / 1 next fast forward last
1
Content available remote FSP and FLTL framework for specification and verification of middle-agents
100%
Bădică A. , Bădică C.
International Journal of Applied Mathematics and Computer Science
|
2011
|
tom 21
|
nr 1
9-25
EN
Agents are a useful abstraction frequently employed as a basic building block in modeling service, information and resource sharing in global environments. The connecting of requester with provider agents requires the use of specialized agents known as middle-agents. In this paper, we propose a formal framework intended to precisely characterize types of middle-agents with a special focus on matchmakers, brokers and front-agents by formally modeling their interactions with requesters and providers. Our approach is based on capturing interaction protocols between requesters, providers and middle-agents as finite state processes represented using FSP process algebra. The resulting specifications are formally verifiable using FLTL temporal logic. The main results of this work include (i) precise specification of interaction protocols depending on the type of middle-agent (this can also be a basis for characterizing types of middle-agents), (ii) improvement of communication between designers and developers and facilitation of formal verification of agent systems, (iii) guided design and implementation of agent-based software systems that incorporate middle-agents.
2
Content available remote FSP and FLTL framework for specification and verification of middle-agents
75%
Bădică A. , Bădică C.
International Journal of Applied Mathematics and Computer Science
|
2011
|
tom Vol. 21, no 1
9-25
EN
Agents are a useful abstraction frequently employed as a basic building block in modeling service, information and resource sharing in global environments. The connecting of requester with provider agents requires the use of specialized agents known as middle-agents. In this paper, we propose a formal framework intended to precisely characterize types of middle-agents with a special focus on matchmakers, brokers and front-agents by formally modeling their interactions with requesters and providers. Our approach is based on capturing interaction protocols between requesters, providers and middle-agents as finite state processes represented using FSP process algebra. The resulting specifications are formally verifiable using FLTL temporal logic. The main results of this work include (i) precise specification of interaction protocols depending on the type of middle-agent (this can also be a basis for characterizing types of middle-agents), (ii) improvement of communication between designers and developers and facilitation of formal verification of agent systems, (iii) guided design and implementation of agent-based software systems that incorporate middle-agents.
3
Content available remote Requirement Elicitation Techniques for Software Projects in Ukrainian IT: An Exploratory Study
63%
Gobov D. , Huchenko I.
Annals of Computer Science and Information Systems
|
2020
|
tom 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.
4
Content available Specyfikacja struktur serwomechanizmów wizyjnych
63%
Kornuta T. , Zieliński C.
Pomiary Automatyka Robotyka
|
2012
|
tom R. 16, nr 2
370-376
PL
W artykule przedstawiono formalną metodę opisu złożonych systemów robotycznych, za pomocą której wyspecyfikowano układy realizujące trzy diametralnie różne zachowania robota: ruch pozycyjny w przestrzeni kartezjańskiej, sterowanie oparte o informację wizyjną pochodzącą z ruchomej kamery zintegrowanej z jego chwytakiem oraz sterowanie wykorzystujące informacje odebraną z nieruchomej kamery. Przedstawione wyniki eksperymentów potwierdzają poprawność stworzonych układów.
EN
The paper presents a formal method of specifying complex robotic systems, applied to the description of three diverse robot behaviors: motion in Cartesian space to a given pose and two types of motions in which the goal was computed on the base of information retrieved from cameras (a camera integrated with the robot gripper and a camera statically mounted above the scene). The presented experimental results confirm the correctness of the developed systems.
5
Content available remote Towards Extending UML's Activity Diagram for the Architectural Modeling, Analysis, and Implementation
63%
Kose M. A. , Ozkaya M.
Annals of Computer Science and Information Systems
|
2020
|
tom 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.
6
Content available Multigraph is: Part 1. A formal description of railway infrastructure for the digital twin of the ETCS application
63%
Kochan A. , Folęga P. , Skirkus R. , Bureika G.
Transport Problems
|
2023
|
tom T. 18, z. 2
43--52
EN
The European Railway Agency has formulated assumptions for a target model of rail transport. Its important premise is digitalization to support the communication and transport services that the railways will make available to the public in the future. Part of the digitalization process is the digital description of the railway infrastructure in a formalized form to allow algorithmic processing. The formal description of infrastructure is not a new issue. However, attempts made so far have not resulted in a permanent definition of a generally accessible formalism allowing for a coherent representation of the physical railway infrastructure in a digital form. This paper presents the results of work carried out within the research project Digital Railway-The Digital Twin of the ETCS Application-Virtual Prototyping and Simulation of Operational Scenarios.
7
Content available remote Modeling and Verification using Different Notations for CPSs: The One-Water-Tank Case Study
51%
Staroletov S. , Schulte H. , Baar T. , Konyukhov I. , Shilov N. , Rozov A. , Liakh T. , Zyubin V.
Annals of Computer Science and Information Systems
|
2021
|
tom 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
8
Content available remote The Syntax of a Multi-Level Production Process Modeling Language
51%
Vještica M. , Dimitrieski V. , Kordić S. , Ristić S. , Luković I. , Pisarić M.
Annals of Computer Science and Information Systems
|
2020
|
tom Vol. 21
751--760
EN
The fourth industrial revolution introduces changes in traditional manufacturing systems and creates basis for a lot-size-one production. The complexity of production processes is significantly increased, alongside the need to enable efficient process simulation, execution, monitoring, real-time decision making and control. The main goal of our research is to define a methodological approach and a software solution in which the Model-Driven Software Development (MDSD) principles and Domain-Specific Modeling Languages (DSMLs) are used to create a framework for the formal description and automatic execution of production processes. In that way production process models are used as central artefacts to manage the production. In this paper, we propose a DSML which can be used to create production process models that are suitable for automatic generation of executable code. The generated code is used for automatic execution of production processes within a simulation or a shop floor.
9
Content available remote Formalization of software risk assessment results in legal metrology based on ISO/IEC 18045 vulnerability analysis
44%
Esche M. , Salwiczek F. , Grasso Toro F.
Annals of Computer Science and Information Systems
|
2019
|
tom Vol. 18
443--447
EN
The Measuring Instruments Directive sets down essential requirements for measuring instruments subject to legal control in the EU. It dictates that a risk assessment must be performed before such instruments are put on the market. Because of the increasing importance of software in measuring instruments, a specifically tailored software risk assessment method has been previously developed and published. Related research has been done on graphical representation of threats by attack probability trees. The final stage is to formalize the method to prove its reproducibility and resilience against the complexity of future instruments. To this end, an inter-institutional comparison of the method is currently being conducted across national metrology institutes, while the weighing equipment manufacturers' association CECIP has provided a new measuring instrument concept, as a significant example of complex instruments. Based on the results of the comparison, a template to formalize the software risk assessment method is proposed here.
10
Content available remote Synteza funkcji należnościowych stacyjnego systemu srk
44%
Zabłocki W.
Zeszyty Naukowo-Techniczne Stowarzyszenia Inżynierów i Techników Komunikacji w Krakowie. Seria: Materiały Konferencyjne
|
2009
|
tom Nr 91, z. 149
523-548
PL
W artykule przedstawiono zarys metody formalizacji systemu srk. Podstawą formalizacji są własności drogi przebiegu analizowane zgodnie z zasadami bezpieczeństwa ze szczególnym uwzględnieniem funkcji sprzeczności dróg przebiegów. Zaproponowana metoda formalizacji definiuje uporządkowane statyczne i dynamiczne struktury danych oraz relacje. Struktury informacji są podstawą konstrukcji relacji, które pozwalają sformułować funkcje i inne relacje zależnościowe systemu srk, a w tym i funkcje sprzeczności dróg przebiegów. Opis formalny relacji i funkcji zależnościowych umożliwia zredagowanie równań zależnościowych warunkujących algorytmizację sterowania. Rezultatem powyższych badań jest formalny (matematyczny) model systemu srk. Model i zbudowany na jego podstawie symulator stanowią narzędzia badawcze, które pozwalają nie tylko wnioskować o systemie srk, a także tworzyć system rzeczywisty.
EN
The outline of the method of rail traffic control systems have been presented in the paper. The features of routing analysed according to safety rules including in particular functions of contradictory functions are the basis of formalisation. The proposed formalisation method defines static and dynamic ordered database structures and relations. The information structures are the basis for creating the relations that allow defining functions and other interlocking relations of rail traffic control facilities including functions of contradictory routings. The formal description of interlocking relations and functions allows defining interlocking equations qualifying control algorithmisation. The result of research is formal (mathematic) model of rail traffic control system. Model and the simulator, constructed basing on it, compose the research tools used for drawing conclusions on rail traffic control facilities and for creating real facilities.
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ć.