Preferencje help
Widoczny [Schowaj] Abstrakt
Liczba wyników

Znaleziono wyników: 16

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

help Ogranicz wyniki do:
first rewind previous Strona / 1 next fast forward last
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.
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.
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.
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.
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.
6
Content available Concurrent systems modeling with CCL
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.
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.
8
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.
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.
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.
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.
12
Content available remote Application of formal methods for hardware/software co-design of embedded systems
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.
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.
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.
15
Content available Timed concurrent state machines
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.
16
Content available remote Systematyczna analiza poprawności w wytwarzaniu bezpiecznego oprogramowania
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.
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ć.