scholarly journals Pemodelan dan Verifikasi Formal Protokol EE-OLSR dengan UPPAAL CORA

2016 ◽  
Vol 10 (1) ◽  
pp. 93
Author(s):  
Rachmat Wahid Saleh Insani ◽  
Reza Pulungan
Keyword(s):  
Model Checking ◽  
Energy Efficient ◽  
Timed Automata ◽  
Packet Transmission ◽  
Model Checker ◽  
Link State ◽  
Internet Users ◽  
Information And Communication ◽  
Fully Automatic ◽  
Verification Process

Information and Communication Technology systems is a most important part of society.  These systems are becoming more and more complex and are massively encroaching on daily life via the Internet and all kinds of embedded systems. Communication protocols are one of the ICT systems used by Internet users. OLSR protocol is a wireless network communication protocol with proactive, and based on link-state algorithm. EE-OLSR protocol is a variant of OLSR that is able to prolong the network lifetime without losses of performance.Protocol verification process generally be done by simulation and testing. However, these processes unable to verify there are no subtle error or design flaw in protocol. Model Checking is an algorithmic method runs in fully automatic to verify a system. UPPAAL is a model checker tool to model, verify, and simulate a system in Timed Automata.UPPAAL CORA is model checker tool to verify EE-OLSR protocol modelled in Linearly Priced Timed Automata, if the protocol satisfy the energy efficient property formulated by formal specification language in Weighted Computation Tree Logic syntax. Model Checking Technique to verify the protocols results in the protocol is satisfy the energy efficient property only when the packet transmission traffic happens.

scholarly journals Model-Checking Speculation-Dependent Security Properties: Abstracting and Reducing Processor Models for Sound and Complete Verification

Electronics ◽  
2019 ◽  
Vol 8 (9) ◽  
pp. 1057
Author(s):  
Gianpiero Cabodi ◽  
Paolo Camurati ◽  
Fabrizio Finocchiaro ◽  
Danilo Vendraminetto
Keyword(s):  
Model Checking ◽  
Formal Verification ◽  
High Performance ◽  
State Of The Art ◽  
Realistic Model ◽  
Bounded Model Checking ◽  
Sensitive Information ◽  
Model Checker ◽  
Verification Process ◽  
Verification Techniques

Spectre and Meltdown attacks in modern microprocessors represent a new class of attacks that have been difficult to deal with. They underline vulnerabilities in hardware design that have been going unnoticed for years. This shows the weakness of the state-of-the-art verification process and design practices. These attacks are OS-independent, and they do not exploit any software vulnerabilities. Moreover, they violate all security assumptions ensured by standard security procedures, (e.g., address space isolation), and, as a result, every security mechanism built upon these guarantees. These vulnerabilities allow the attacker to retrieve leaked data without accessing the secret directly. Indeed, they make use of covert channels, which are mechanisms of hidden communication that convey sensitive information without any visible information flow between the malicious party and the victim. The root cause of this type of side-channel attacks lies within the speculative and out-of-order execution of modern high-performance microarchitectures. Since modern processors are hard to verify with standard formal verification techniques, we present a methodology that shows how to transform a realistic model of a speculative and out-of-order processor into an abstract one. Following related formal verification approaches, we simplify the model under consideration by abstraction and refinement steps. We also present an approach to formally verify the abstract model using a standard model checker. The theoretical flow, reliant on established formal verification results, is introduced and a sketch of proof is provided for soundness and correctness. Finally, we demonstrate the feasibility of our approach, by applying it on a pipelined DLX RISC-inspired processor architecture. We show preliminary experimental results to support our claim, performing Bounded Model-Checking with a state-of-the-art model checker.

scholarly journals Is your Model Checker on Time? On the Complexity of Model Checking for Timed Modal Logics

1999 ◽  
Vol 6 (32) ◽  
Author(s):  
Luca Aceto ◽  
Francois Laroussinie
Keyword(s):  
Computational Complexity ◽  
Model Checking ◽  
Timed Automata ◽  
Structural Complexity ◽  
Modal Logics ◽  
System Model ◽  
Model Checker ◽  
Program Complexity

This paper studies the structural complexity of model checking<br />for (variations on) the specification formalisms used in the tools CMC<br />and Uppaal, and fragments of a timed alternation-free mu-calculus. For<br />each of the logics we study, we characterize the computational complexity<br />of model checking, as well as its specification and program complexity,<br />using timed automata as our system model.

scholarly journals On Memory-Block Traversal Problems in Model Checking Timed Systems

2000 ◽  
Vol 7 (3) ◽  
Author(s):  
Fredrik Larsson ◽  
Paul Pettersson ◽  
Wang Yi
Keyword(s):  
Model Checking ◽  
State Space ◽  
Operating Systems ◽  
Memory Management ◽  
Timed Automata ◽  
Model Checker ◽  
Timed Systems ◽  
Memory Block ◽  
Start Up

A major problem in model-checking timed systems is the<br />huge memory requirement. In this paper, we study the memory-block<br />traversal problems of using standard operating systems in exploring the<br />state-space of timed automata. We report a case study which demonstrates<br />that deallocating memory blocks (i.e. memory-block traversal)<br />using standard memory management routines is extremely time-consuming.<br />The phenomenon is demonstrated in a number of experiments by<br />installing the Uppaal tool on Windows95, SunOS 5 and Linux. It seems<br />that the problem should be solved by implementing a memory manager<br />for the model-checker, which is a troublesome task as it is involved in<br />the underlining hardware and operating system. We present an alternative<br />technique that allows the model-checker to control the memory-block<br />traversal strategies of the operating systems without implementing<br />an independent memory manager. The technique is implemented in the<br />Uppaal model-checker. Our experiments demonstrate that it results in<br />significant improvement on the performance of Uppaal. For example, it<br />reduces the memory deallocation time in checking a start-up synchronisation<br />protocol on Linux from 7 days to about 1 hour. We show that the<br />technique can also be applied in speeding up re-traversals of explored<br />state-space.

Using Timed Automata for Modeling the Clocks of Distributed Embedded Systems

2010 ◽  
pp. 172-193 ◽  
Author(s):  
Guillermo Rodriguez-Navas ◽  
Julian Proenza ◽  
Hans Hansson ◽  
Paul Pettersson
Keyword(s):  
Model Checking ◽  
Embedded Systems ◽  
Embedded System ◽  
Timed Automata ◽  
Model Checker ◽  
Distributed Embedded Systems ◽  
Temporal Behaviour ◽  
System Designer ◽  
Functional Aspects ◽  
Time Systems

Model checking is a widely used technique for the formal verification of computer systems. However, the suitability of model checking strongly depends on the capacity of the system designer to specify a model that captures the real behaviour of the system under verification. For the case of real-time systems, this means being able to realistically specify not only the functional aspects, but also the temporal behaviour of the system. This chapter is dedicated to modeling clocks in distributed embedded systems using the timed automata formalism. The different types of computer clocks that may be used in a distributed embedded system and their effects on the temporal behaviour of the system are introduced, together with a systematic presentation of how the behaviour of each kind of clock can be modeled. The modeling is particularized for the UPPAAL model checker, although it can be easily adapted to other model checkers based on the theory of timed automata.

scholarly journals Linear Parametric Model Checking of Timed Automata

2001 ◽  
Vol 8 (5) ◽  
Author(s):  
Thomas S. Hune ◽  
Judi Romijn ◽  
Mariëlle Stoelinga ◽  
Frits W. Vaandrager
Keyword(s):  
Model Checking ◽  
State Space ◽  
Timed Automata ◽  
Parametric Model ◽  
Model Checker ◽  
Linear Parameter ◽  
Emptiness Problem ◽  
Full Class ◽  
Parameter Constraints ◽  
Published Paper

<p>We present an extension of the model checker Uppaal capable<br /> of synthesizing linear parameter constraints for the correctness of<br />parametric timed automata. The symbolic representation of the (parametric)<br /> state-space is shown to be correct. A second contribution of this<br />paper is the identification of a subclass of parametric timed automata<br />(L/U automata), for which the emptiness problem is decidable, contrary<br />to the full class where it is know to be undecidable. Also we present a<br />number of lemmas enabling the verification effort to be reduced for L/U<br />automata in some cases. We illustrate our approach by deriving linear<br />parameter constraints for a number of well-known case studies from the<br />literature (exhibiting a flaw in a published paper).</p>

scholarly journals IMITATOR 3: Synthesis of Timing Parameters Beyond Decidability

2021 ◽  
pp. 552-565
Author(s):  
Étienne André
Keyword(s):  
Model Checking ◽  
Real Time ◽  
Timed Automata ◽  
Robustness Analysis ◽  
Parametric Model ◽  
Timing Constraints ◽  
Real Time Systems ◽  
Model Checker ◽  
Time Systems ◽  
Timed Model Checking

AbstractReal-time systems are notoriously hard to verify due to nondeterminism, concurrency and timing constraints. When timing constants are uncertain (in early the design phase, or due to slight variations of the timing bounds), timed model checking techniques may not be satisfactory. In contrast, parametric timed model checking synthesizes timing values ensuring correctness. takes as input an extension of parametric timed automata (PTAs), a powerful formalism to formally verify critical real-time systems. extends PTAs with multi-rate clocks, global rational-valued variables and a set of additional useful features. We describe here the new features and algorithms offered by  3, that moved along the years from a simple prototype dedicated to robustness analysis to a standalone parametric model checker for timed systems.

Fepchecker: An Automatic Model Checker for Verifying Fairness and Non-Repudiation of Security Protocols in Web Service

2016 ◽  
Vol 26 (04) ◽  
pp. 563-585 ◽  
Author(s):  
Xiaohong Li ◽  
Jiayi Xu ◽  
Guangquan Xu ◽  
Jianye Hao ◽  
Xiaoru Li ◽  
...  
Keyword(s):  
Model Checking ◽  
Web Service ◽  
Current Model ◽  
Model Checker ◽  
Cryptographic Primitives ◽  
Application Range ◽  
Pi Calculus ◽  
Security Properties ◽  
Verification Process ◽  
Critical Model

Ensuring the fairness and non-repudiation in the security exchange protocol of web service is critical. Model checking is often used for automatic verification for the security properties of protocol. However, the current model checker tools cannot support formalizing protocols with cryptographic primitives, specifying properties with linear temporal logic (LTL) and automatically generating resilient intruder model simultaneously and the application range of them is severely limited. To solve this problem, a model checker Fepchecker is proposed to verify the fairness and non-repudiation properties, which are critical features in security exchange protocols. Firstly, applied pi-calculus is extended to specify the protocols, and the LTL assertion is used for precisely describing fairness and non-repudiation. Secondly, an intruder model is applied to construct their behavior sequences automatically and the protocol sessions and message pattern are used to alleviate the states explosion problem. Thirdly, in our model checking algorithm, the fairness and non-repudiation properties are verified based on Labeled Transition System (LTS) semantics model and the MakeOneMove method is used to explore the state space on-the-fly in the verification process. Finally, Fepchecker is applied to verify six representative protocols and the results show that Fepchecker can effectively verify their fairness and non-repudiation properties.

scholarly journals Model Checking Techniques applied to the design of Web Services

2007 ◽  
Vol 10 (2) ◽  
Author(s):  
Gregorio Dıaz ◽  
Emilia M. Cambronero ◽  
Juan J. Pardo ◽  
Valentın Valero ◽  
Fernando Cuartero
Keyword(s):  
Model Checking ◽  
Web Services ◽  
Timed Automata ◽  
Critical Role ◽  
Verification And Validation ◽  
Time Constraints ◽  
Model Checker

In previous work we have presented the generation of WS-CDL and WS-BPEL documents. In this paper we show the unification of both generations. The aim is to generate correct WS-BPEL skeleton documents from WS-CDL documents by using the Timed Automata as an intermediary model in order to check the correctness of the generated Web Services with Model Checking Techniques. The model checker used is UPPAAL, a well known tool in theoretical and industrial cases that performs the verification and validation of Timed Automata. Note that our interest is focused on Web services where the time constraints play a critical role.

Design and Testing of an Experimental IPv4-to-IPv6 Transition Network

2006 ◽  
Vol 3 (1) ◽  
pp. 27
Author(s):  
Mustaffa Samad
Keyword(s):  
Transition Period ◽  
Internet Protocol ◽  
Smooth Transition ◽  
Internet Users ◽  
Ipv6 Transition ◽  
Information And Communication ◽  
Ipv6 Networks ◽  
And Migration ◽  
Set Up ◽  
Design And Testing

The Internet has been an integral part of the Information and Communication Technology (ICT) community in recent years. New internet users have been growing steadily over the years. This has lead to the depletion of new Internet Protocol (IP) addresses worldwide. To overcome this predicament, the new Internet Protocol version 6 (IPv6) had been introduced. The existing Internet Protocol version 4 (IPv4) is expected to be eventually replaced by this IPv6. The changeover from IPv4 to IPv6 is expected to be implemented progressively. During this transition period, these two protocols are expected to coexist for a number of years. IPv4-to-IPv6 transition tools have been designed to facilitate a smooth transition from IPv4 to IPv6. The two most basic IPv4-to-IPv6 transition tools available are the hybrid stack mechanism and tunneling. Tunneling is the encapsulation of IPv6 traffic within IPv4 packets so they can be sent over an IPv4 infrastructure. This project was initiated to set up an experimental IPv6 testbed, in order to study the performance as well as transition and migration issues of IPv6 networks under controlled conditions. This paper looks at how tunneling can be performed over existing internetwork infrastructure at Fakulti Kejuruteraan Elektrik (FKE), UiTM.

Shifting Dynamics of Contention in the Digital Age

2020 ◽  
Author(s):  
Jun Liu
Keyword(s):  
Information And Communication Technologies ◽  
Mobile Communication ◽  
Communication Technologies ◽  
Digital Age ◽  
Chinese Society ◽  
Internet Users ◽  
Communicative Practice ◽  
Political Contention ◽  
Information And Communication ◽  
Everyday Resistance

Over the past decades, waves of political contention involving the use of information and communication technologies have swept across the globe. The phenomenon stimulates the scholarship on digital communication technologies and contentious collective action to thrive as an exciting, relevant, but highly fragmentary and contested field with disciplinary boundaries. To advance the interdisciplinary understanding, Shifting Dynamics of Contention in the Digital Age outlines a communication-centered framework that articulates the intricate relationship between technology, communication, and contention. It further prods us to engage more critically with existing theories from communication, sociology, and political science on digital technologies and political movements. Given the theoretical endeavor, Shifting Dynamics of Contention in the Digital Age systematically explores, for the first time, the influence of mobile technology on political contention in China, the country with the world’s largest number of mobile and Internet users. Using first-hand in-depth interview and fieldwork data, it tracks the strategic choice of mobile phones as repertoires of contention, illustrates the effective mobilization of mobile communication on the basis of its strong and reciprocal social ties, and identifies the communicative practice of forwarding officially alleged “rumors” as a form of everyday resistance. Through this ground-breaking study, Shifting Dynamics of Contention in the Digital Age presents a nuanced portrayal of an emerging dynamics of contention—both its strengths and limitations—through the embedding of mobile communication into Chinese society and politics.

Sign in / Sign up

Export Citation Format

Share Document