Spelling suggestions: "subject:"model checking anda simulationlation"" "subject:"model checking anda motionsimulation""
1 |
A Bigraphical Framework for Modeling and Simulation of UAV-based Inspection ScenariosGrzelak, Dominik, Lindner, Martin 11 April 2024 (has links)
We present a formal modeling approach for the design and simulation of Multi-Unmanned Aerial Vehicle (multi-UAV) inspection scenarios, where planning is based on model checking. As demonstration, we formalize and simulate a compositional UAV inspection system of a solar park using bigraphical reactive systems, which introduce the notion of time-varying bigraphs. Specifically, the UAV system is modeled as a process-algebraic expression, whose semantics is a bigraph state in a labeled transition system.
The underlying Multi-Agent Path Finding problem is solved model-theoretically using Planning-by-Model-Checking. It solves the inherently connected collision-free path planning problem for multiple UAVs subject to contexts and local conditions. First, a bigraph is constructed algebraically, which can be decomposed systematically into separate parts with interfaces. The layered composite model accounts for location, navigation, UAVs, and contexts, which enables simple configuration and extension (changeability). Second, the executable operational semantics of our formal bigraph model are given by bigraphical reactive systems, where rules constitute the behavioral component of our model. Rules reconfigure the bigraph to simulate state changes, i.e., they allow to alter the conditions under which UAVs are permitted to move.
Properties can be attached to nodes of the bigraph and evaluated in a simulation over the traces of the transition system according to some cost-based policies.
In essence, the inherent multi-UAV path planning problem of our scenario is formulated as a reachability problem and solved by model checking the generated transition system. The bigraph-algebraic expression also allows us to reason about potential parallelization opportunities when moving UAVs. Moreover, we sketch how to directly simulate the bigraph specification in a ROS-based Gazebo simulation by examining the inspection and monitoring of a solar park as an application.
The reactive system specification provides the blueprint for analysis, simulation, implementation and execution. Thus, the same algorithm used for verification is used as well for the simulation in ROS/Gazebo to execute plans.:1 Introduction
2 Overview: Scenario Description and Formal Modeling Approach
3 Background: Bigraphs and Model Checking
4 Construction of the UAV System via Composition
5 Making the Drones Fly: Executable Model Semantics
6 Collision-Free Path Planning Problem
7 Prototypical Implementation
8 Discussion
9 Related Work
10 Conclusion
A UAV State Machine
B Bigraphical Reactive Systems
C RPO/IPO Semantic
|
2 |
Automatic Reasoning Techniques for Non-Serializable Data-Intensive ApplicationsGowtham Kaki (7022108) 14 August 2019 (has links)
<div>
<div>
<div>
<p>The performance bottlenecks in modern data-intensive applications have induced
database implementors to forsake high-level abstractions and trade-off simplicity and
ease of reasoning for performance. Among the first casualties of this trade-off are the
well-known ACID guarantees, which simplify the reasoning about concurrent database
transactions. ACID semantics have become increasingly obsolete in practice due
to serializable isolation – an integral aspect of ACID, being exorbitantly expensive.
Databases, including the popular commercial offerings, default to weaker levels of
isolation where effects of concurrent transactions are visible to each other. Such weak
isolation guarantees, however, are extremely hard to reason about, and have led to
serious safety violations in real applications. The problem is further complicated
in a distributed setting with asynchronous state replications, where high availability
and low latency requirements compel large-scale web applications to embrace weaker
forms of consistency (e.g., eventual consistency) besides weak isolation. Given the
serious practical implications of safety violations in data-intensive applications, there
is a pressing need to extend the state-of-the-art in program verification to reach non-
serializable data-intensive applications operating in a weakly-consistent distributed
setting.
</p>
<p>This thesis sets out to do just that. It introduces new language abstractions, program logics, reasoning methods, and automated verification and synthesis techniques
that collectively allow programmers to reason about non-serializable data-intensive
applications in the same way as their serializable counterparts. The contributions
</p>
</div>
</div>
<div>
<div>
<p>xi
</p>
</div>
</div>
</div>
<div>
<div>
<div>
<p>made are broadly threefold. Firstly, the thesis introduces a uniform formal model to
reason about weakly isolated (non-serializable) transactions on a sequentially consistent (SC) relational database machine. A reasoning method that relates the semantics
of weak isolation to the semantics of the database program is presented, and an automation technique, implemented in a tool called ACIDifier is also described. The
second contribution of this thesis is a relaxation of the machine model from sequential
consistency to a specifiable level of weak consistency, and a generalization of the data
model from relational to schema-less or key-value. A specification language to express
weak consistency semantics at the machine level is described, and a bounded verification technique, implemented in a tool called Q9 is presented that bridges the gap
between consistency specifications and program semantics, thus allowing high-level
safety properties to be verified under arbitrary consistency levels. The final contribution of the thesis is a programming model inspired by version control systems that
guarantees correct-by-construction <i>replicated data types</i> (RDTs) for building complex distributed applications with arbitrarily-structured replicated state. A technique
based on decomposing inductively-defined data types into <i>characteristic relations</i> is
presented, which is used to reason about the semantics of the data type under state
replication, and eventually derive its correct-by-construction replicated variant automatically. An implementation of the programming model, called Quark, on top of
a content-addressable storage is described, and the practicality of the programming
model is demonstrated with help of various case studies.
</p>
</div>
</div>
</div>
|
Page generated in 0.132 seconds