| | SLO | ENG | Piškotki in zasebnost

Večja pisava | Manjša pisava

Iskanje po katalogu digitalne knjižnice Pomoč

Iskalni niz: išči po
išči po
išči po
išči po
* po starem in bolonjskem študiju


1 - 5 / 5
Na začetekNa prejšnjo stran1Na naslednjo stranNa konec
Curiosity, checking, and knowing : a virtue-theoretical perspective
Nenad Miščević, 2023, drugi znanstveni članki

Opis: In his important and original book, Knowing and Checking, Guido Melchior provides advice on how to tackle skepticism. I argue that his analysis points to a possible virtue-theoretic answer to skepticism, which I call the restraint solution, i.e., activate your self-trust and restrain your inquisitiveness! It leads one to the ideal of bounded reflective curiosity: when it comes to knowledge, we should restrain our second-order, reflective curiosity and stay content with the somewhat Moorean trust in ordinary everyday beliefs. We can preserve our ordinary, first-order vigilance and investigative interest (curiosity) without falling into skeptical over-caution which is basically a reflective, second-order vicious attitude.
Ključne besede: checking inquiry, curiosity, virtue epistemology
Objavljeno v DKUM: 19.03.2024; Ogledov: 141; Prenosov: 6
.pdf Celotno besedilo (824,49 KB)
Gradivo ima več datotek! Več...

Improved formal verification of SDN-based firewalls by using TLA+
Tatjana Kapus, 2023, izvirni znanstveni članek

Opis: 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.
Ključne besede: firewalls, formal specification, formal verification, logic, model checking, software defined networking
Objavljeno v DKUM: 04.12.2023; Ogledov: 199; Prenosov: 9
.pdf Celotno besedilo (1,24 MB)
Gradivo ima več datotek! Več...

Modelling medium access control in IEEE 802.15.4 nonbeacon-enabled networks with probabilistic timed automata
Tatjana Kapus, izvirni znanstveni članek

Opis: This paper concerns the formal modelling of medium access control in nonbeacon-enabled IEEE 802.15.4 wireless personal area networks with probabilistic timed automata supported by the PRISM probabilistic model checker. In these networks, the devices contend for the medium by executing an unslotted carrier sense multiple access with collision avoidance algorithm. In the literature, a model of a network which consists of two stations sending data to two different destination stations is introduced. We have improved this model and, based on it, we propose two ways of modelling a network with an arbitrary number of sending stations, each having its own destination. We show that the same models are valid representations of a star-shaped network with an arbitrary number of stations which send data to the same destination station. We also propose how to model such a network if some of the sending stations are not within radio range of the others, i.e. if they are hidden. We present some results obtained for these models by probabilistic model checking using PRISM.
Ključne besede: wireless personal area network, medium access control, hidden station, formal specification, probabilistic model checking
Objavljeno v DKUM: 15.06.2017; Ogledov: 1224; Prenosov: 361
.pdf Celotno besedilo (2,25 MB)
Gradivo ima več datotek! Več...

ACTLW - an action-based computation tree logic with unless operator
Robert Meolic, Tatjana Kapus, Zmago Brezočnik, 2008, izvirni znanstveni članek

Opis: 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.
Ključne besede: formal verification, model checking, action-based temporal logic, fixed point, mutual-exclusion algorithm
Objavljeno v DKUM: 01.06.2012; Ogledov: 2398; Prenosov: 101
URL Povezava na celotno besedilo

Iskanje izvedeno v 5.04 sek.
Na vrh
Logotipi partnerjev Univerza v Mariboru Univerza v Ljubljani Univerza na Primorskem Univerza v Novi Gorici