Wyniki wyszukiwania - BazTech

1

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.

2

Odwzorowanie działania protokołu dwufazowego zatwierdzania z wieloma uczestnikami za pomocą kolorowanej sieci Petriego

Iwaniak M., Khadzyhonov W.

Studia Informatica

|

2013

|

Vol. 34, nr 2A

57--69

PL

W artykule przedstawiono wykorzystanie kolorowanej sieci Petriego do przedstawienia modelu i symulacji działania protokołu 2PC z wieloma uczestnikami (ang. Two-phase commit), czyli protokołu dwufazowego zatwierdzania. Wprowadzono podstawowe pojęcia dotyczące kolorowanych sieci Petriego. Opisano działanie protokołu dwufazowego zatwierdzania. Zaprezentowano model odwzorowujący działanie protokołu 2PC dla więcej niż jednego uczestnika. Za pomocą odpowiedniego doboru znakowań początkowych przeprowadzono analizę osiągalnych rozwiązań dla różnych sytuacji, które mogą zaistnieć w trakcie realizacji transakcji rozproszonej z wykorzystaniem protokołu 2PC.

EN

In this work the usage of Colored Petri Net for modeling and simulation of Two Phase Commit protocol with multiple cohorts is presented. Brief overview of Colored Petri Nets is introduced. Two-Phase Commit protocol is briefly described than introduced as Colored Petri Net model. By initial marking adaptation a few scenarios for 2PC protocol are presented with the use of the reachability analysis.

3

Kolorowana sieć Petriego jako model systemu podejmowania decyzji kredytowej

Dec G., Jędrzejec B., Rząsa W.

Studia Informatica

|

2010

|

Vol. 31, nr 2A

203-212

PL

W artykule opisano model formalny i implementację systemu ekspertowego (SE) do podejmowania decyzji kredytowych. SE projektowany jest jako zbiór powiązanych tabel decyzyjnych (TD). Jako model tego SE zastosowano kolorowaną sieć Petriego (CPN), na którą odwzorowano strukturę SE oraz sposób wyznaczania wartości przez TD. Utworzono moduł podejmowania decyzji kredytowych, który jest częścią systemu informatycznego przeznaczonego dla bankowości.

EN

The paper describes a formal model and implementation of an expert system (ES) for a credit decision making. The ES is designed as a set of related decision tables (DT). The Colored Petri Net (CPN) is adopted as a model of the ES. The structure and behavior of the ES is mapped into the CPN. A software module for a credit decision making is developed and deployed to a computer system for banking.