Wyniki wyszukiwania - BazTech

1

Prototyping Self-healing Behavior for NASA Swarm-based Systems with ASSL

Vassev Emil, Hinchey Mike

TASK Quarterly : scientific bulletin of Academic Computer Centre in Gdansk

|

2021

|

Vol. 25, No 2

203--231

EN

Autonomic computing promises computer systems capable of self-management, which augurs great promise for unmanned spacecraft. Such spacecraft are extremely appropriate for deep space exploration missions because the former bring onboard intelligence and less reliance on control links. The Autonomic System Specification Language (ASSL) is a framework for developing autonomic systems. As part of our research on ASSL, we have successfully specified autonomic properties, verified their consistency, and generated implementation for both the NASA ANTS (Autonomous Nano-Technology Swarm) concept mission and the NASA Voyager mission. This paper presents concrete results on the use of ASSL to develop a self-healing behavior model for NASA ANTS swarm-based exploration missions. Here, we present specification and implementation results. Moreover, we experiment with the ASSL-generated code to demonstrate that the implemented ANTS system is capable of self-management in respect of the specified self-healing model.

2

Functional safety verification of train control procedure in train-centric CBTC by colored Petri net

Lin Junting, Xu Qian

Archives of Transport

|

2020

|

Vol. 54, iss. 2

43--58

EN

Communication-based Train Control (CBTC) system is a widely-used signaling system. There is an increasing demand for innovating the traditional ground-centric architecture. With the application of train-train communication, object control and other advanced techniques, Train-centric CBTC (TcCBTC) system is expected to be the most promising tendency of train control system. The safe tracking interval would be reduced as well as the life-cycle costs. Formal methods play an essential role in the development of safety-critical systems, which provides an early integration of the verifiable design process. In the paper, the architecture design of TcCBTC is first analyzed. The official system specification of TcCBTC has not issued, so it takes efforts to perform the systematic summarization of the functional requirements. Secondly, we propose an integrated framework that combines the Colored Petri Net (CPN) models with the functional safety verification of the underlying systems. Functional safety depends on the logic accuracy and is a part of overall safety. The framework also specifies what kinds of functions, behaviors or properties need to be verified. The train control procedure of TcCBTC is regarded as the link among new functional modules, thus it is chosen as the modelling content. Thirdly, the scenarios and the color sets are prepared. Models are established with the novel design thought from top to bottom. Simulation and testing are implemented during the model establishment to discover the apparent errors. Lastly, the model checking by state space is performed. All possible states are checked in detail. Standard behavioral properties and other user-defined properties are verified by state space report and ASK-CTL (Computation Tree Logic) queries, respectively. Verification results reveal that the models are reasonable to depict the dynamic behaviors of train control procedure. The functional safety properties are satisfied and prepared for further drafting the system functional specification.

3

Satisfiability Calculus : An Abstract Formulation of Semantic Proof Systems

Lopez Pombo Carlos G., Castro Pablo F., Aguirre Nazareno M., Maibaum Thomas S. E.

Fundamenta Informaticae

|

2019

|

Vol. 166, nr 4

297--347

EN

The theory of institutions, introduced by Goguen and Burstall in 1984, can be thought of as an abstract formulation of model theory. This theory has been shown to be particularly useful in computer science, as a mathematical foundation for formal approaches to software construction. Institution theory was extended by a number of researchers, José Meseguer among them, who, in 1989, presented General Logics , wherein the model theoretical view of institutions is complemented by providing (categorical) structures supporting the proof theory of any given logic. In other words, Meseguer introduced the notion of proof calculus as a formalisation of syntactical deduction, thus “implementing” the entailment relation of a given logic. In this paper we follow the approach initiated by Goguen and introduce the concept of Satisfiability Calculus. This concept can be regarded as the semantical counterpart of Meseguer’s notion of proof calculus, as it provides the formal foundations for those proof systems that resort to model construction techniques to prove or disprove a given formula, thus “implementing” the satisfiability relation of an institution. These kinds of semantic proof methods have gained a great amount of interest in computer science over the years, as they provide the basic means for many automated theorem proving techniques.

4

Kolory projektowania

Brzeziński K. M.

Przegląd Telekomunikacyjny + Wiadomości Telekomunikacyjne

|

2015

|

nr 2-3

103--106

PL

Pokazano, że rozumienie i stosowanie ważnych i popularnych w dziedzinie ICT terminów black-box, grey-box i white-box jest obarczone wadami. Zaproponowano alternatywne, bardziej systematyczne podejście. Przedyskutowano konsekwencje tej propozycji w kontekście projektowania w ogóle, a w szczególności – testowania jako nieodłącznego aspektu projektowania.

EN

Within ICT, the use of the important notions and terms: black-box, grey-box and white-box is inconsistent .To address this problem, a more systematic approach is proposed, in which "colours" are treated as properties of systems boundaries, and the latter are explicitly divided into knowledge and access boundaries. The consequences of this proposal for design, and in particular for testing as a part of design, are discussed.

5

Formal Description of Alvis Language with α0 System Layer

Szpyrka M., Matyasik P., Mrówka R., Kotulski L.

Fundamenta Informaticae

|

2014

|

Vol. 129, nr 1/2

161--171

EN

The paper presents a formal description of a subset of the Alvis language designed for the modelling and formal verification of concurrent systems. Alvis combines possibilities of a formal models verification with flexibility and simplicity of practical programming languages. Alvis provides a graphical modelling of interconnections among agents and a high level programming language used for the description of agents behaviour. Its semantic depends on the so-called system layer. The most universal system layer α0, described in the paper, makes Alvis similar to other formal languages like Petri nets, process algebras, time automata, etc.

6

Model checking processes specified in join-calculus algebra

Maludziński S., Dobrowolski G.

Computer Science

|

2014

|

Vol. 15 (1)

61--74

EN

This article presents a model checking tool used to verify concurrent systems specified in join-calculus algebra. The temporal properties of systems under verification are expressed in CTL logic. Join-calculus algebra, with its operational semantics defined by a chemical abstract machine, serves as the basic method for the specification of concurrent systems and their synchronization mechanisms, allowing for the examination of more complex systems. The described model checker is a proof of concept for the utilization of new methodologies of formal system specification and verification in software engineering practice.

7

Concurrent systems modeling with CCL

Kułakowski K.

Automatyka / Automatics

|

2012

|

Vol. 16, no. 2

115-125

EN

One of the challenges facing software engineering is to conduct research into new methods of modeling systems. The CCL notation shown in the article tries to follow in this direction. The solutions and methods presented here indicate its practical application to modeling complex eomputer systems using the struetural, dataflowcentric approach. The basis for the proposed integration between CCL and struetural methods is the newly defined externalization mechanism. It allows the details of inter-process communication to be abstracted away, thereby reducing the size of the submodels which are subject to further verification. Thanks to the methods adopted here, the overall picture of the system becomes morę readable for humans, and, due to the significant submodel state space reduction, the effective use of formal methods for their analysis becomes possible.

PL

Jednym z podstawowych zadań związanych z inżynierią oprogramowania jest szukanie nowych i optymalizacja istniejących metod modelowania systemów informatycznych. Przedstawiona w pracy notacja CCL stara się wpisywać w ten nurt badań. Prezentowane podejście pokazuje jej użyteczność w kontekście użycia metod strukturalnych (diagramy przepływu danych) do modelowania złożonych systemów informatycznych. Podstawą proponowanej integracji pomiędzy CCL i metodami modelowania strukturalnego jest nowowprowadzone pojęcie eksternalizacji. Pozwala ono abstrahować od szczegółów implementacyjnych komunikacji międzyprocesowej, redukując tym samym wielkość modeli podlegających dalszej weryfikacji. Dzięki przyjętemu rozwiązaniu modele stają się bardziej czytelne dla projektantów, oraz dzięki znaczącej redukcji przestrzeni stanów, możliwe staje się efektywne wykorzystanie metod formalnych w celu ich dalszej analizy.

8

Causal Behavioural Profiles - Efficient Computation, Applications and Evaluation

Weidlich M., Mendling J., Polyvyanyy A., Weske M.

Fundamenta Informaticae

|

2011

|

Vol. 113, nr 3/4

399-435

EN

Analysis of behavioural consistency is an important aspect of software engineering. In process and service management, consistency verification of behavioural models has manifold applications. For instance, a business process model used as system specification and a corresponding workflow model used as implementation have to be consistent. Another example would be the analysis to what degree a process log of executed business operations is consistent with the corresponding normative process model. Typically, existing notions of behaviour equivalence, such as bisimulation and trace equivalence, are applied as consistency notions. Still, these notions are exponential in computation and yield a Boolean result. In many cases, however, a quantification of behavioural deviation is needed along with concepts to isolate the source of deviation. In this article, we propose causal behavioural profiles as the basis for a consistency notion. These profiles capture essential behavioural information, such as order, exclusiveness, and causality between pairs of activities of a process model. Consistency based on these profiles is weaker than trace equivalence, but can be computed efficiently for a broad class of models. In this article, we introduce techniques for the computation of causal behavioural profiles using structural decomposition techniques for sound free-choice workflow systems if unstructured net fragments are acyclic or can be traced back to S- or T-nets. We also elaborate on the findings of applying our technique to three industry model collections.

9

Introduction to modelling embedded systems with Alvis

Szpyrka M., Matyasik P., Mrówka R., Witalec W., Baniewicz J., Kotulski L.

Automatyka / Akademia Górniczo-Hutnicza im. Stanisława Staszica w Krakowie

|

2011

|

T. 15, z. 2

435-442

EN

Alvis is a modelling language for concurrent and real-time systems. It combines hierarchical graphical modelling with a Haskell-based high level programming language. The graphical layer is used to define data and control flow among agents. The code layer is used to describe the behaviour of individual agents. An Alvis model is transformed into a labelled transition system (LTS) that is used for formal verification of the model. The paper discusses some aspects of modelling embedded systems with Alvis.

PL

Alvis jest językiem modelowania rozwijanym z myślą o systemach współbieżnych w szczególności systemach wbudowanych. Łączy on w sobie graficzny język modelowania, przeznaczony do definiowania połączeń komunikacyjnych między agentami, z językiem programowania wysokiego poziomu, przeznaczonym do definiowania zachowania poszczególnych agentów. W artykule przedstawiono wybrane aspekty modelowania systemów wbudowanych z użyciem języka Alvis.

10

Towards the Safety Verification of Real-Time Systems with the Coq Proof Assistant

Tveretina O.

Journal of Automation Mobile Robotics and Intelligent Systems

|

2009

|

Vol. 3, No. 1

30-32

EN

Hybrid systems involve the interaction of discrete and continuous dynamics. Hybrid systems have been used as a mathematical model for many safety critical applications. One of the most important analysis problems of hybrid systems is the reachability problem. In this paper we argue that the proof assistant Coq can be used for the hybrid systems verification. An example of a train crossing control is provided.

11

Improving Dependability of Automation for Free Electron Laser FLASH

Kosęda B., Szmuc T., Cichalewski W.

Journal of Automation Mobile Robotics and Intelligent Systems

|

2009

|

Vol. 3, No. 1

33-39

EN

Free-electron laser FLASH (260-meter-long machine) is a pilot facility for the forthcoming XFEL (3 km). Along with growth of the experiment, service and maintenance are becoming so complex that certain degree of automation seems to be inevitable. The main purpose of the automation software is to facilitate operators with computer-aided supervision of several hardware/software subsystems. The efforts presented in this contribution concern elaboration of general framework for designing and development of automation software for the FLASH. The toolkit facilitates specification, implementation, testing and formal verification. The ultimate goal of the framework is to systematize the way of automation software development and to improve its dependability. At present usefulness of the tools is being evaluated by testing the automation software for single RF-power station of the FLASH.

12

A system automating repairs of IT systems

Kamiński M.

Elektronika : konstrukcje, technologie, zastosowania

|

2009

|

Vol. 50, nr 11

54-57

EN

This paper presents two problems that are important nowadays: the problem of IT systems monitoring and the problem of repairing them. It shows the developed solution, aimed to automate the existing industrial repair process and to integrate it with the existing monitoring Solutions and mechanisms. Described solution is a part of a bigger whole, called the Repair Management Framework (RMF). This paper presents also briefly a case study related to the developed and implemented system, showing how it was used to solve the real problem regarding the functioning of database management systems.

PL

Artykuł ten dotyczy dwóch istotnych problemów: problemu monitorowania systemów IT oraz problemu ich naprawiania. Zaprezentowano w nim rozwiązanie umożliwiające automatyzację istniejących procesów naprawczych oraz ich integrację z przemysłowymi systemami i mechanizmami monitorującymi. Opisane rozwiązanie jest częścią większego projektu, nazwanego RMF (Repair Management Framework). W artykule tym zamieszczono również skrótowe studium przypadku dotyczące wytworzonego oraz zaimplementowanego systemu, pokazujące w jaki sposób został on użyty do rozwiązywania rzeczywistego problemu dotyczącego funkcjonowania systemów zarządzania bazami danych.

13

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.

14

From formal methods to implementation based on Petri Nets model of concurrent systems

Wojciechowski J.

Pomiary Automatyka Kontrola

|

2007

|

R. 53, nr 5

132-134

EN

Purpose of this work is to suggest a path from formal methods to implementation in designing concurrent system, thus helping further stages of systems development to go on. Author focuses on mapping of nonhierarchical Coloured Petri Nets model to class model of the system in Java and C language. Author extends among others formal model with information which would imply generation of class models from formal model, conforming to Java specification and C language, making continuous integration possible. The whole cycle would be presented with changed Petri Nets model of simple concurrent system.

PL

Celem pracy jest zaproponowanie ścieżki przejścia od modelu formalnego systemu opisanego siecią Petriego do implementacji. Autor skupia się na rzutowaniu niehierarchicznych modeli sieci do modelu klas odpowiadającemu obiektowemu paradygmatowi programowania języka Java i proceduralnemu dla języka C. Autor rozszerza model formalny o informację umożliwiającą dokonanie konwersji do modelu klas i procedur. Cały cykl będzie zaprezentowany na prostym systemie współbieżnym.

15

Mapping of petri net formal model of concurrent system to class model with aspect of polymorphism in object oriented paradigm

Wojciechowski J.

Mikroelektronika i Informatyka : prace naukowe

|

2007

|

Z. nr 7

167-170

EN

Models are developed in meny areas of engineering as means of understending the requirements for a system and assessing the chances of a design. In sofware development process, models range from the graphical representations of data i.e. entity-relationship diagram and functionality i.e. UML to the formal mathematical representation of functional and temporal behavior using Petri nets. Aspect of extracting polymorphism dependency from model towards implementation in OO design is presented in this article.

PL

Celem pracy jest zaproponowanie ścieżki przejścia od modelu formalnego systemu opisanego siecią Petriego do implementacji na szczególnym skupieniu się na ekstrakcji cech obiektowych związanych z cechą polimorfizmu modelu. Autor skupia się na rzutowaniu nie hierarchicznych modeli sieci do modelu klas odpowiadającemu obiektowemu paradygmatowi programowania języka Java. Autor rozszerza model formalny o informację umożliwiajacą dokonanie konwersji do modelu klas uwzględniajac polimorfizm modelu. Cały cykl będzie reprezentowany na przypadkach użycia występujących w modelu.

16

Timed concurrent state machines

Daszczuk W. B.

Computer Science

|

2007

|

Vol. 8, Spec. Ed

23-36

EN

Timed Concurrent State Machines are an application of Alur Timed Automata concept to coincidence-based (rather than interleaving) CSM modeling technique. TCSM support the idea of testing automata, allowing to specify time properties easier than temporal formulas. Also, calculation of a global state space in real-time domain (Region Concurrent State Machines) is defined, allowing to storę a verified system in ready-to-verification form, and to multiply it by various testing automata.

PL

Współbieżne maszyny stanowe z czasem TCSM są aplikacją automatów czasowych Alura w środowisku koincydencyjnym współbieżnych maszyn czasowych CSM (w przeciwieństwie do środowisk przeplotowych). TCSM pasują do idei automatów testujących, które pozwalają wyspecyfikować zależności czasowe łatwiej niż poprzez formuły temporalne. Ponadto zdefiniowano sposób wyznaczania globalnej przestrzeni stanów w dziedzinie czasu (współbieżne maszyny stanowe regionów RCSM), co pozwala przechowywać badany system w postaci gotowej do weryfikacji i mnożyć go przez różne automaty testujące.

17

Systematyczna analiza poprawności w wytwarzaniu bezpiecznego oprogramowania

Szmuc T., Rogus G.

Pomiary Automatyka Kontrola

|

2005

|

R. 51, nr 9 bis

288--290

PL

W artykule opisano zastosowanie języka formalnej specyfikacji LOTOS do wspomagania systematycznej analizy poprawności. Scharakteryzowano możliwości tego języka (tzw. style projektowe), jak również opisano koncepcję analizy poprawności. Przedstawiono również ramowe algorytmy analizy poprawności z wykorzystaniem pakietu CADP.

EN

An application of LOTOS formal specification language for systematic correctness verification support is described in the paper. Basic possibilities (the so-called design frameworks) of this language are described, as well as the correctness concept is discussed. General algorithms for the correctness analysis using CADP package are also described.