Wyniki wyszukiwania - BazTech

1

Using splitter ordering heuristics to improve bisimulation in probabilistic model checking

Mohagheghi Mohammadsadegh, Salehi Khayyam

Computer Science

|

2025

|

T. 26 (2)

49--75

EN

Model checking is used to verify computer-based and cyber-physical systems, but faces challenges due to state space explosion. Bisimulation minimization reduces states in transition systems, easing this issue. Probabilistic bisimulation further simplifies models with stochastic behaviors. Recent techniques aim to improve the time complexity of iterative methods in computing probabilistic bisimulation for stochastic systems with nondeterministic behaviors. In this paper, we propose several techniques to accelerate iterative processes to partition the state space of a given probabilistic model to its bisimulation classes. The first technique applies two ordering heuristics for choosing splitter blocks. The second technique uses hash tables to reduce the running time and the average time complexity of the standard iterative method. The proposed approaches are implemented and run on several conventional case studies and reduce the running time by one order of magnitude on average.

2

Formal verification of STPA with model checking

Kwon Ryeonggu, Kwon Gihwon

Scientific Journal of Gdynia Maritime University

|

2023

|

nr 125

7--24

EN

As technology advances, hardware-centric systems are rapidly moving towards software-centric ones, and their complexity is rapidly increasing. In particular, systems directly related to safety require thorough verification. Model checking exhaustively explores the state space of the abstracted system to check whether properties written in a logical formula are achieved. In this paper, the control algorithm of the controller is verified using model checking to discover risk scenarios during the STPA steps. Two case studies are conducted using the widely used model checkers NuSMV and UPPAAL. We then explain the empirical results and compare two model checkers based on their characteristics. Finally, we discuss the benefits of applying model checking in the process of STPA.

3

Unbounded Model Checking for ATL

Kański Michał, Niewiadomski Artur, Kacprzak Magdalena, Penczek Wojciech, Nabiałek Wojciech

Studia Informatica : systems and information technology

|

2021

|

Vol. 1-2(25)

5--22

EN

In this paper, we deal with verification of multi-agent systems represented as concurrent game structures. To express properties to be verified, we use Alternating-Time Temporal Logic (ATL) formulas. We provide an implementation of symbolic model checking for ATL and preliminary, but encouraging experimental results.

4

Parametric Schedulability Analysis of a Launcher Flight Control System under Reactivity Constraints.

André Étienne, Coquard Emmanuel, Fribourg Laurent, Jerray Jawher, Lesens David, Keller Jörg, Penczek Wojciech

Fundamenta Informaticae

|

2021

|

Vol. 182, nr 1

31--67

EN

The next generation of space systems will have to achieve more and more complex missions. In order to master the development cost and duration of such systems, an alternative to a manual design is to automatically synthesize the main parameters of the system. In this paper, we present an approach for the specific case of the scheduling of the flight control of a space launcher. The approach requires two successive steps: (1) the formalization of the problem to be solved in a parametric formal model and (2) the synthesis of the model parameters with a tool. We first describe the problem of the scheduling of a launcher flight control, then we show how this problem can be formalized with parametric stopwatch automata; we then present the results computed by the parametric timed model checker IMITATOR. We enhance our model by taking into consideration the time for switching context, and we compare the results to those obtained by other tools classically used in scheduling.

5

Causal Reasoning for Safety in Hennessy Milner Logic

Caltais Georgiana, Mousavi Mohammad Reza, Singh Hargurbir

Fundamenta Informaticae

|

2020

|

Vol. 173, nr 2-3

217--251

EN

Determining and computing root causes in system failures is a significant issue in science and engineering. In this paper, we introduce a notion of causality for explaining counter-examples in system analysis based on formal models. The counter-examples are produced by checking for hazardous situations expressed in the Hennessy-Milner Logic, in the context of Labelled Transition System models. We also introduce CauseJMu, a tool for automatically identifying such causal computations within a system model. CauseJMu relies on encoding causality in terms of an extension of Hennessy-Milner Logic to recursive formulae with data. The encodings enable deciding whether a certain computation is causal or not, using the mCRL2 model checker.

6

Activity Networks with Delays an Application to Toxicity Analysis

Delaplace F., Di Giusto C., Giavitto J. -L, Klaudel H., Spicher A.

Fundamenta Informaticae

|

2018

|

Vol. 160, nr 1/2

119--142

EN

ANDy, Activity Networks with Delays, is a discrete framework aiming at the qualitative modeling of time-dependent activities. The modular and expressive syntax makes ANDy suitable for a concise and natural modeling of time-dependent biological systems (i.e., regulatory pathways). Activities involve entities playing the role of activators, inhibitors or products of biochemical network operation. Activities may have a given duration, i.e., the time required to obtain results. An entity may represent an object (e.g., an agent, a biochemical species or a family of thereof) with a local attribute, a state denoting its level (e.g., concentration, strength). Entity levels may change as a result of an activity or may decay gradually as time passes by. The semantics of ANDy is formally given via high-level Petri nets ensuring this way some modularity. As main results we show that ANDy systems have finite state representations even for potentially infinite processes and it well adapts to the modeling of toxic behaviors. As an illustration, we present a classification of toxicity properties and give some hints on how they can be verified on ANDy systems with existing tools. A case study on blood glucose regulation is provided to exemplify the ANDy framework and the toxicity properties.

7

A Dynamic-Logical Characterization of Solutions to Sight-limited Extensive Games

Liu C., Liu F., Su K.

Fundamenta Informaticae

|

2018

|

Vol. 158, nr 1/3

149--169

EN

An unrealistic assumption in classical extensive game theory is that the complete game tree is fully perceivable by all players. To weaken this assumption, a class of games (called games with short sight) was proposed in literature, modelling the game scenarios where players have only limited foresight of the game tree due to bounded resources and limited computational ability. As a consequence, the notions of equilibria in classical game theory were refined to fit games with short sight. A crucial issue that thus arises is to determine whether a strategy profile is a solution to a game. To study this issue and address the underlying idea and theory on players’ decisions in such games, we adopt a logical way. Specifically, we develop a logic called DLS through which features of these games are demonstrated. More importantly, it enables us to characterize the solutions to these games via formulas of this logic. Moreover, we study the algorithm for model checking DLS, which is shown to be PTIME-complete in the size of the model. This work not only provides an insight into a more realistic model in game theory, but also enriches the possible applications of logic.

8

Cooperation of multiple autonomous robots and analysis of their swarm behawior

Czejdo B., Daszczuk W. B., Grabski W., Bhattacharya S.

Autobusy : technika, eksploatacja, systemy transportowe

|

2018

|

R. 19, nr 12

872--879

EN

In this paper, we extended previous studies of cooperating autonomous robots to include situations when environmental changes and changes in the number of robots in the swarm can affect the efficiency to execute tasks assigned to the swarm of robots. We have presented a novel approach based on partition of the robot behavior. The sub-diagrams describing sub-routs allowed us to model advanced interactions between autonomous robots using limited number of state combinations avoiding combinatorial explosion of reachability. We identified the systems for which we can ensure the correctness of robots interactions. New techniques were presented to verify and analyze combined robots’ behavior. The partitioned diagrams allowed us to model advanced interactions between autonomous robots and detect irregularities such as deadlocks, lack of termination etc. The techniques were presented to verify and analyze combined robots’ behavior using model checking approach. The described system, Dedan verifier, is still under development. In the near future, timed and probabilistic verification are planned.

PL

W artykule opisano kontynuację wcześniejszych badań dotyczących współpracy autonomicznych robotów wewnątrz budynku. Obejmują one obejmują sytuacje, w których zmiany środowiska i zmiana liczby robotów w roju mogą poprawić lub pogorszyć efektywność wykonywania zadań przypisanych do roju robotów. Zaprezentowaliśmy nowatorskie podejście z wykorzystaniem dzielenia zachowań robota na zachowania składowe. Poddiagramy opisujące kładowe podmarszruty pozwoliły nam modelować zaawansowane interakcje między autonomicznymi robotami w oparciu o ograniczoną liczbę kombinacji zachowań, unikając eksplozji kombinatorycznej przestrzeni osiągalności. Opisano systemy, dla których możemy zapewnić poprawność interakcji robotów i zaprezentowano techniki weryfikacji i analizy zachowań połączonych robotów. Diagramy podzielone na partycje pozwoliły nam modelować zaawansowane interakcje pomiędzy autonomicznymi robotami i wykrywać nieprawidłowości, takie jak zakleszczenia, brak terminacji itp. Przedstawiono techniki weryfikacji i analizy złożonych zachowań robotów za pomocą techniki weryfikacji modelowej. Opisany system weryfikacji, Dedan, jest wciąż rozwijany. W niedalekiej przyszłości planowana jest weryfikacja z czasem rzeczywistym i probabilistyczna.

9

Łukasiewicz μ-calculus

Mio M., Simpson A.

Fundamenta Informaticae

|

2017

|

Vol. 150, nr 3/4

317--346

EN

The paper explores properties of the Łukasiewicz μ-calculus, or Łμ for short, an extension of Łukasiewicz logic with scalar multiplication and least and greatest fixed-point operators (for monotone formulas). We observe that Łμ terms, with n variables, define monotone piece-wise linear functions from [0, 1]n to [0, 1]. Two effective procedures for calculating the output of Łμ terms on rational inputs are presented. We then consider the Łukasiewicz modal μ-calculus, which is obtained by adding box and diamond modalities to Łμ. Alternatively, it can be viewed as a generalization of Kozen’s modal μ-calculus adapted to probabilistic nondeterministic transition systems (PNTS’s). We show how properties expressible in the well-known logic PCTL can be encoded as Łukasiewicz modal μ-calculus formulas. We also show that the algorithms for computing values of Łukasiewicz μ-calculus terms provide automatic (albeit impractical) methods for verifying Łukasiewicz modal μ-calculus properties of finite rational PNTS’s.

10

SyLVaaS : System Level Formal Verification as a Service

Mancini T., Mari F., Massini A., Melatti I., Tronci E.

Fundamenta Informaticae

|

2016

|

Vol. 149, nr 1/2

101--132

EN

The goal of System Level Formal Verification is to show system correctness notwithstanding uncontrollable events (disturbances), as for example faults, variations in system parameters, external inputs, etc. This may be achieved with an exhaustive Hardware In the Loop Simulation based approach, by considering all relevant scenarios in the System Under Verification (SUV) operational environment. In this paper, we present SyLVaaS, a Web-based tool enabling Verification as a Service (VaaS). SyLVaaS implements an assume-guarantee approach to (Hardware In the Loop Simulation based) System Level Formal Verification. SyLVaaS takes as input a finite state automaton defining the SUV operational environment and computes, using parallel algorithms deployed in a cluster infrastructure, a set of highly optimised simulation campaigns, which can be executed in an embarrassingly parallel fashion (i.e., with no communication among the parallel processes) on a set of Simulink instances, using a platform independent Simulink driver downloadable from the SyLVaaS Web site. As the actual simulation is carried out at the user premises (e.g., on a private cluster), SyLVaaS allows full Intellectual Property protection of the SUV model as well as of the user verification flow. The simulation campaigns computed by SyLVaaS randomise the verification order of operational scenarios and this enables, at anytime during the parallel simulation activity, the estimation of the completion time and the computation of an upper bound to the Omission Probability, i.e., the probability that there is a yet-to-be-simulated operational scenario which violates the property under verification. This information supports graceful degradation in the verification activity. We show effectiveness of the SyLVaaS algorithms and infrastructure by evaluating the system on case studies consisting of input operational environments entailing up to 35 641 501 scenarios related to the system level verification of models from the Simulink distribution (namely, Inverted Pendulum on a Cart and Fuel Control System).

11

Tools and Methods for RTCP-Nets Modeling and Verification

Szpyrka M., Biernacki J., Biernacka A.

Archives of Control Sciences

|

2016

|

Vol. 26, no. 3

339--365

EN

RTCP-nets are high level Petri nets similar to timed colored Petri nets, but with different time model and some structural restrictions. The paper deals with practical aspects of using RTCP-nets for modeling and verification of real-time systems. It contains a survey of software tools developed to support RTCP-nets. Verification of RTCP-nets is based on coverability graphs which represent the set of reachable states in the form of directed graph. Two approaches to verification of RTCP-nets are considered in the paper. The former one is oriented towards states and is based on translation of a coverability graph into nuXmv (NuSMV) finite state model. The later approach is oriented towards transitions and uses the CADP toolkit to check whether requirements given as μ-calculus formulae hold for a given coverability graph. All presented concepts are discussed using illustrative examples.

12

Jak zapewnić poprawności działania programów komputerowych?

Greniewski M. J.

Studia i Materiały / Europejska Uczelnia Informatyczno-Ekonomiczna w Warszawie

|

2015

|

Nr 2(10)

1--15

PL

Narasta problem skutków błędów w oprogramowaniu. Konieczna stała się zmiana podejścia – zapewnienie poprawności działania programów komputerowych. Dotyczy to głównie programów współbienych – reaktywnych. Metody formalne pozwalają na zastąpienie metody testowania programów (o wątpliwej skuteczności) metodami walidacji, czyli dowodzenia poprawności działania przez sprawdzanie stanów osiagąnych przez model sterowania programu. Podstawą jest pomysł użycia logiki temporalnej do opisu działania programów współbiernych Amira Pnueli z 1977 roku, który został rozwinięty na początku lat osiemdziesiątych ubiegłego wieku w teorie przez Clarke’a, Emersona oraz Sifakisa (uhonorowani w 2007 r. ACM A.M. Turing Award). Wzmiankowana teorie zastosowano w języku modelowania Promela oraz procesorze Spin (Simple Promela Interpreter) autorstwa zespołu Gerarda J. Holzmanna (uhonorowanego w 2002 r. ACM Software System Award).

EN

There is a growing tendency of the effects of bugs in the software. It becomes necessary to change the approach – to ensure proper operation of computer programs. This applies mainly to concurrent programs – reactive ones. Formal methods allow substitution of the method of testing programs (of dubious efficacy) by validation methods, which is proving the correctness of the action – by checking the status achieved by the control model program. The basis is the idea of using temporal logic to describe the actions of concurrent programs by Amir Pnueli from 1977, further developed in the early eighties of the last century into the theory of Clarke, Emerson and Sifakis (honored in 2007 ACM A.M. Turing Award). The theory mentioned above, was used in modeling language Promela and Spin processor (Simple Promela Interpreter) by Gerard J. Holzmann team (which won the 2002 ACM Software System Award).

13

Underapproximating ATL with Imperfect Information and Imperfect Recall

Jamroga W., Knapik M.

Prace Instytutu Podstaw Informatyki Polskiej Akademii Nauk

|

2015

|

Nr 1032

1--16

EN

We investigate the correspondence between model checking of af-AMCi and ATLir , on the example of reachability. We identify some of the reasons for the fact that these logics are of uncomparable expressivity. These observations form the basis for a novel method for underapproximating ATLir by means of fixed-point calculations. We introduce a special version of the next-step operator, called Persistent Imperfect Next-Step Operator h_iF and show how it can be used to define a new version of reachability that carries to ATLir.

PL

W pracy badane są związki pomiędzy weryfikacją modelową Bezpamięciowej Logiki Temporalnej Czasu Alternującego z Niepełną Informacją ATLir i Epistemicznego Alternującego Mu-Rachunku af-AMCi. Jak pokazano, naturalne uogólnienia pojęcia osiągalności z ATLir -a do af-AMCi nie przynoszą dobrych efektów: osiągalność w af-AMCi nie pociąga za sobą osiągalności w ATLir . Po zidentyfikowaniu części powodów, dla których tak się dzieje, zaproponowano nową wersję operatora następnego kroku, który pozwala na przybliżanie osiągalności w ATLir przy pomocy obliczeń stałopunktowych.

14

A symbolic shortest path algorithm for computing subgame-perfect Nash equilibria

Góngora P. A, Rosenblueth D. A.

International Journal of Applied Mathematics and Computer Science

|

2015

|

Vol. 25, no. 3

577--596

EN

Consider games where players wish to minimize the cost to reach some state. A subgame-perfect Nash equilibrium can be regarded as a collection of optimal paths on such games. Similarly, the well-known state-labeling algorithm used in model checking can be viewed as computing optimal paths on a Kripke structure, where each path has a minimum number of transitions. We exploit these similarities in a common generalization of extensive games and Kripke structures that we name “graph games”. By extending the Bellman–Ford algorithm for computing shortest paths, we obtain a model-checking algorithm for graph games with respect to formulas in an appropriate logic. Hence, when given a certain formula, our model-checking algorithm computes the subgame-perfect Nash equilibrium (as opposed to simply determining whether or not a given collection of paths is a Nash equilibrium). Next, we develop a symbolic version of our model checker allowing us to handle larger graph games. We illustrate our formalism on the critical-path method as well as games with perfect information. Finally, we report on the execution time of benchmarks of an implementation of our algorithms.

15

Model Checking Temporal Properties of Reaction Systems

Męski A., Penczek W., Rozenberg G.

Prace Instytutu Podstaw Informatyki Polskiej Akademii Nauk

|

2014

|

Nr 1028

1--28

EN

This paper defines a temporal logic for reaction systems (RSTL). The logic is interpreted over the models for the context restricted reaction systems that generalize standard reaction systems by controlling context sequences. Moreover, a translation from the context restricted reaction systems into boolean functions is defined in order to be used for a symbolic model checking for RSTL over these systems. Finally, model checking for RSTL is proved to be PSPACE-complete.

PL

Praca wprowadza logikę temporalną dla systemów reakcyjnych (RSTL), która jest interpretowana w modelach dla systemów reakcyjnych z ograniczeniami kontekstów. Systemy te uogólniają standardowe systemy reakcyjne przez wprowadzenie ograniczeń kontrolujących dopuszczalne konteksty. Ponadto, przedstawiono translację z systemów reakcyjnych z ograniczeniami kontekstów do formuł boolowskich, która umożliwia symboliczną weryfikację modelową dla tych systemów oraz RSTL. Wykazano również, że problem weryfikacji modelowej dla RSTL jest problemem PSPACE-zupełnym.

16

On-the-fly Trace Generation Approach to the Security Analysis of Cryptographic Protocols: Coloured Petri Nets-based Method

Permpoontanalarp Y., Sornkhom P.

Fundamenta Informaticae

|

2014

|

Vol. 130, nr 4

423--466

EN

Most Petri nets-based methods that have been developed to analyze cryptographic protocols provide the analysis of one attack trace only. Only a few of them offer the analysis of multiple attack traces, but they are rather inefficient. Analogously, the limitation of the analysis of one attack trace occurs in most model checking methods for cryptographic protocols. In this paper, we propose a very simple but practical Coloured Petri nets-based model checking method for the analysis of cryptographic protocols, which overcomes these limitations. Our method offers an efficient analysis of multiple attack traces. We apply our method to two case studies which are TMN authenticated key exchanged protocol and Micali's contract signing protocol. Surprisingly, our simple method is very efficient when the numbers of attack traces and states are large. Also, we find many new attacks in those protocols.

17

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.

18

Translation of probabilistic games in J2TADD

Rataj A.

Theoretical and Applied Informatics

|

2013

|

Vol. 25, No. 3-4

157--182

EN

A new version of J2TADD - a translator from Java to automatons- is described, which adds support for a translation of Markov processes with non-dcterministic players, that can form coalitions, which in turn strive for different aims. In order to ease the definition of a probabilistic game using a plain Java application, several new constructs, and also a special library, are supported within the input language.Ranges on variables or on expressions can be defined, what helps in checking the self-consistency of a model, and can also make the solving of the model faster.

PL

Artykuł prezentuje nową wersję translatora J2TADD. Dodane zostało tłumaczenie procesów markowowskich z niedelerministycznymi graczami, mogącymi formować koalicje mające różne cele. By ułatwić pisanie gier probabilistycznych dodane zostało kilka specyficznych dla gier konstrukcji, jak również specjalna biblioteka. Aktualnej wersja posiada również kilka innych usprawnień: ● wybory, które są zwykłymi wyrażeniami języka Java, jednak hc tłumaczy je na specyficzne dla automatów rozgałęzienia probabilistyczne lub niedeterministyczne; ● można definiować dopuszczalne wartości zmiennych, co pomaga w sprawdzaniu wewnętrznej spójności modelu, a także może przyspieszyć jego rozwiązanie; ● różne metody specyfikacji niezmienników i warunków zegarowych. Artykuł prezentuje jako przykład prostą grę probabilistyczną, modelującą rynek lokalnego dostawcy energii elektrycznej. W ramach przykładu omawiane są wersje automatów do rozwiązywania metodą analityczną i symulacyjną.

19

Weryfikowanie specyfikacji wymagań sterownika logicznego za pomocą diagramów aktywności UML, logiki temporalnej LTL i środowiska NuSMV

Grobelna I., Grobelny M.

Pomiary Automatyka Robotyka

|

2013

|

R. 17, nr 10

188--192

PL

W artykule przedstawiono ideę zastosowania diagramów aktywności UML do specyfikacji wymagań dotyczących zachowania sterownika logicznego. Lista wymagań podlegających weryfikacji zwykle definiowana jest bezpośrednio za pomocą formuł logiki temporalnej. Użycie przyjaznych dla użytkownika, powszechnie znanych i wykorzystywanych diagramów pozwala na prostsze i bardziej intuicyjne zapisanie wymagań. Diagramy są następnie formalnie przekształcane do formuł liniowej logiki temporalnej (LTL).

EN

The article introduces an idea to use UML activity diagrams [1-5] for specification of requirements regarding logic controller behavior. Requirements list to be verified [14] (using model checking technique [6, 7]) is usually directly defined using temporal logic formulas [12, 15]. Using user-friendly, commonly known and practiced diagrams allows to easier and more intuitively write down the requirements easier and more intuitively. Activity diagrams are then formally transformed into linear temporal logic (LTL) formulas. In this paper some sample UML activity diagrams which specify global properties are presented, together with their interpretation using LTL logic. To perform model checking process, model description (based i.e. on a control interpreted Petri net [8] or indirectly on an UML activity diagram [11]), and requirements list are needed. Afterwards it is checked, whether defined properties are satisfied in specified model description. If a requirement cannot be fulfilled, appropriate counterexample is generated allowing to localize error source. The article is structured as follows. Section 1 is an introduction. Background of a logic controller specification and its verification is presented in section 2. A novel approach to logic controller requirements definition using activity diagrams is shown in section 3. The paper ends with a short summary.

20

Weryfikacja modelowa hierarchicznej specyfikacji sterownika logicznego

Grobelna I., Grobelny M.

Pomiary Automatyka Kontrola

|

2013

|

R. 59, nr 8

796--798

PL

Specyfikacja zachowania projektowanego urządzenia powinna uwzględniać wszystkie elementy behawioralne. Z uwagi na złożoność projektowanych systemów szczególnie istotną rolę odgrywa możliwość dekompozycji. Z wykorzystaniem hierarchii można podzielić specyfikację na logiczne elementy połączone ze sobą na diagramach wyższego poziomu. W artykule przedstawiono zagadnienia związane z formalną weryfikacją hierarchicznych specyfikacji sterownika logicznego wyrażonych za pomocą interpretowanych sieci Petriego oraz diagramów aktywności języka UML.

EN

Specification of a designed logic controller should include all behavioral aspects. By complex systems design decomposition is especially valuable. Specification can be divided into parts using hierarchy. Logical elements are joined together at higher-level diagrams. The paper focuses on formal verification [1] of logic controller hierarchical specification by means of UML activity diagrams and interpreted Petri nets. Although hierarchy itself is presented in the considered specification techniques in different ways (complex activities by UML activity diagrams and macro-places/ macrotransitions by Petri nets), it is possible to use both techniques together in one project and to transform anytime one diagram into the another [5, 9, 10] (example in Figs. 1 and 2). In the transformation process, UML activity diagram actions correspond to Petri net transitions [7, 8]. Model checking [2, 3] of hierarchical specification can be performed step by step, e.g. by means of the NuSMV tool [11]. Rule-based specification (based on a Petri net) can be checked against behavioral properties [12, 13] expressed by temporal logic formulas [4]. Macroplaces can be verified separately (Fig. 3 considering local properties) and/or concurrently (Fig. 4, Fig. 5 considering mutual correlation and global properties). Next, the whole Petri net with macroplaces can be checked (Fig. 6). Sometimes it is convenient to verify a complete net (not hierarchical), like in [14]. Formal verification of specification can significantly increase its quality, and the support for hierarchy simplifies complex systems verification.