| | SLO | ENG | Cookies and privacy

Bigger font | Smaller font

Search the digital library catalog Help

Query: search in
search in
search in
search in
* old and bologna study programme


1 - 3 / 3
First pagePrevious page1Next pageLast page
Improved formal verification of SDN-based firewalls by using TLA+
Tatjana Kapus, 2023, original scientific article

Abstract: In an article published in IEEE Access in 2020, researchers present an approach to using TLA + for the formal verification of whether a network of SDN (Software-Defined Networking) switches implements the filtering rules of a given monolithic firewall. The distributed as well as monolithic firewalls are specified with TLA + . It is shown that the correctness of the former with respect to the latter can be verified automatically by using the TLC model checker. The main contributions of this paper are the following improvements of that approach. Firstly, by specifying switches without using any variables, the time needed for the model checking is reduced significantly. For example, the verification of the same networks takes a few seconds with the new approach and does not end after several hours with the previous one. Secondly, the following problem is solved. With the latter, if a monolithic firewall allows a packet to pass through, all the paths in the distributed firewall which the packet is routed on must allow the same. Otherwise, the model checker proclaims the distributed firewall to be in error. We present an additional approach to the verification, which gives a positive answer if at least one of the paths allows the packet to pass through.
Keywords: firewalls, formal specification, formal verification, logic, model checking, software defined networking
Published in DKUM: 04.12.2023; Views: 127; Downloads: 8
.pdf Full text (1,24 MB)
This document has many files! More...

Applying automated model extraction for simulation and verification of real-life SDL specification with spin
Boštjan Vlaovič, Aleksander Vreže, Zmago Brezočnik, 2017, original scientific article

Abstract: Formally defined Specification and Description Language (SDL) is used for the design and specification of complex safety-critical systems. Each change in the specification of the product should be immediately checked formally against the requirements’ specification. This paper presents semi-automated system abstraction, automated model extraction, simulation, and formal verification of real-life complex SDL specification. Sound algorithms implemented in our sdl2pml automated model extraction tool preserve all properties of the SDL system. Sdl2pml includes our model of discrete time, abstraction, and support for all relevant SDL functionality and constructs such as dynamic process creation, rational data types, and communication with more than one process instance. To the best of our knowledge, most of them are not supported by any other known approach. We use our SpinRCP tool for simulation and formal verification of the extracted model with the Spin model checker. We demonstrate the applicability of our approach on ISDN User adaptation protocol from SI3000 Softswitch. The extracted Promela model is the largest one ever processed by Spin. We have shown that Spin simulation and model checking can be applied successfully to such huge models.
Keywords: formal specifications, automated extraction, formal languages, simulation, formal verification, model cheking, SDL, Promela, SpinRCP, Sdl2pml
Published in DKUM: 03.08.2017; Views: 1258; Downloads: 416
.pdf Full text (13,46 MB)
This document has many files! More...

ACTLW - an action-based computation tree logic with unless operator
Robert Meolic, Tatjana Kapus, Zmago Brezočnik, 2008, original scientific article

Abstract: Model checkers for systems represented by labelled transition systems are not as extensively used as those for systems represented by Kripke structures. This is partially due to the lack of an elegant formal language for property specification which would not be as raw as, for example, HML yet also not as complex as, for example, -calculus. This paper proposes a new action-based propositional branching-time temporal logic ACTLW, which enhances popular computation tree logic (CTL) with the notion of actions in a similar but more comprehensive way than action-based CTL introduced by De Nicola and Vaandrager [R. De Nicola, F.W. Vaandrager, Action versus logics for transition systems, in: Semantics of Systems of Concurrent Processes, Proceedings LITP Spring School on Theoretical Computer Science, LNCS 469, 1990, pp. 407-419]. ACTLW is defined by using temporal operators until and unless only, whereas all other temporal operators are derived from them. Fixed-point characterisation of the operators together with symbolic algorithms for globalmodel checking are shown. Usage of this new logic is illustrated by an example of verification of mutual-exclusion algorithms.
Keywords: formal verification, model checking, action-based temporal logic, fixed point, mutual-exclusion algorithm
Published in DKUM: 01.06.2012; Views: 2281; Downloads: 101
URL Link to full text

Search done in 0.79 sec.
Back to top
Logos of partners University of Maribor University of Ljubljana University of Primorska University of Nova Gorica