Uncertainty on Discrete-Event System Simulation

Uncertainty Propagation methods are well-established when used in modeling and simulation formalisms like differential equations. Nevertheless, until now there are no methods for Discrete-Dynamic Systems. Uncertainty-Aware Discrete-Event System Specification (UA-DEVS) is a formalism for modeling Discrete-Event Dynamic Systems that include uncertainty quantification in messages, states, and event times. UA-DEVS models provide a theoretical framework to describe the models’ uncertainty and their properties. As UA-DEVS models can include continuous variables and non-computable functions, their simulation could be non-computable. For this reason, we also introduce Interval-Approximated Discrete-Event System Specification (IA-DEVS), a formalism that approximates UA-DEVS models using a set of order and bounding functions to obtain a computable model. The computable model approximation produces a tree of all trajectories that can be traversed from the original model and some erroneous ones introduced by the approximation process. We also introduce abstract simulation algorithms for IA-DEVS, present a case study of UA-DEVS, its IA-DEVS approximation and, its simulation results using the algorithms defined.

Approbation of the stochastic group virus protection model

The article discusses the implementation in Java of the stochastic collaborative virus defense model developed within the framework of the Distributed Object-Based Stochastic Hybrid Systems (DOBSHS) model and its analysis. The goal of the work is to test the model in conditions close to the real world on the way to introducing its use in the practical environment. We propose a method of translating a system specification in the SHYMaude language, intended for the specification and analysis of DOBSHS models in the rewriting logic framework, into the corresponding Java implementation. The resulting Java system is deployed on virtual machines, the virus and the group virus alert system are modeled stochastically. To analyze the system we use several metrics, such as the saturation time of the virus propagation, the proportion of infected nodes upon reaching saturation and the maximal virus propagation speed. We use Monte Carlo method with the computation of confidence intervals to obtain estimates of the selected metrics. We perform analysis on the basis of the sigmoid virus propagation graph over time in the presence of the defense system. We implemented two versions of the system using two protocols for transmitting messages between nodes, TCP/IP and UDP. We measured the influence of the protocol type and the associated costs on the defense system effectiveness. To assess the potential of cost reduction associated with the use of different message transmission protocols, we performed analysis of the original DOBSHS model modified to model message transmission delays. We measured the influence of other model parameters important for the next steps towards the practical use of the model. To address the system scalability, we propose a hierarchical approach to the system design to make possible its use with a large number of nodes.

ENHANCEMENT OF STABILITY ON AUTONOMOUS WAYPOINT MISSION OF QUADROTOR USING LQR INTEGRATOR CONTROL

The ability of the quadrotor in the waypoint trajectory tracking becomes an essential requirement in the completion of various missions nowadays. However, the magnitude of steady-state errors and multiple overshoots due to environmental disturbances leads to motion instability. These conditions make the quadrotor experience a shift and even change direction from the reference path. As a result, to minimize steady-state error and multiple overshoots, this study employs a Linear Quadratic Regulator control method with the addition of an Integrator. Comparisons between LQR without Integrator and LQR with Integrator were performed. They were implemented on a quadrotor controller to track square and zig-zag waypoint patterns. From experimental results, LQR without Integrator produce of 2 meters steady-state error and -1.04 meters undershoot average with an accuracy of 64.84 % for square pattern, along 3.19 meters steady-state error, and -1.12 meters undershoot average with an accuracy of 46.73 % for a zig-zag way. The LQR method with integrator produce of 1.06 meters steady-state error with accuracy 94.96 % without multiple-overshoot for square pattern, the 1.06 meters steady-state error, and -0.18 meters undershoot average with an accuracy of 86.49 % for the zig-zag way. The results show that the LQR control method with Integrator can minimize and improve steady-state error and multiple overshoots in quadrotor flight. The condition makes the quadrotor able to flying path waypoints with the correct system specification. ABSTRAK: Kemampuan quadrotor dalam pengesanan lintasan waypoint menjadi syarat penting dalam menyelesaikan pelbagai misi pada masa kini. Walau bagaimanapun, besarnya ralat keadaan mantap dan banyak kelebihan kerana gangguan persekitaran menyebabkan ketidakstabilan pergerakan. Keadaan ini menjadikan quadrotor mengalami pergeseran dan bahkan mengubah arah dari jalur rujukan. Oleh itu, kajian ini menggunakan kaedah kawalan Linear Quadratic Regulator dengan penambahan integrator dalam meminimumkan ralat keadaan mantap dan banyak kelebihan. Perbandingan antara LQR tanpa Integrator dan LQR dengan Integrator dilakukan. Mereka dilaksanakan pada pengawal quadrotor untuk mengesan corak titik jalan persegi dan zig-zag. Dari hasil eksperimen, LQR tanpa Integrator menghasilkan ralat keadaan mantap 2 meter dan -1.04 meter rata-rata undur tembak dengan ketepatan 64.84% untuk corak persegi, sepanjang ralat keadaan tetap 3.19 meter, dan -1.12 meter rata-rata undur bawah dengan ketepatan 46.73 % untuk cara zig-zag. Kaedah LQR dengan integrator menghasilkan ralat keadaan mantap 1.06 meter dengan ketepatan 94.96% tanpa tembakan berlebihan untuk corak segi empat sama, ralat keadaan mantap 1.06 meter, dan rata-rata undur tembak -0.18 meter dengan ketepatan 86.49% untuk zig-zag cara. Hasilnya menunjukkan bahawa kaedah kawalan LQR dengan Integrator dapat meminimumkan dan memperbaiki ralat keadaan mantap dan banyak overhoot dalam penerbangan quadrotor. Keadaan tersebut menjadikan quadrotor dapat terbang ke titik jalan dengan spesifikasi sistem yang betul.

A graph-based data quality analysis in distributed telemedicine systems

Telemedicine is one of the most rapidly developing areas of healthcare and it plays an increasing role in modern medicine. As the amount of data and demand for features increase, the data paths are becoming ever-more complex. Owing to this, it is vital in telemedicine to find a proper balance between consistency and availability under any given circumstances. However, making a trade-off can significantly influence the quality of the data. This study seeks to get an in-depth view of the problem by considering a real-world telemedicine use-case and elaborating the formal system specification of the scenario. After evaluating the specification, the constructed state graph is examined using graph coloring and other graph algorithms.

Metamodel-based formalization of DEVS atomic models

The Discrete-Event System Specification (DEVS) formalism is a modeling formalism based on systems theory that provides a general methodology for hierarchical construction of reusable models in a modular way. When concrete DEVS models are developed using programming languages, it is difficult to ensure they conform to their formal model. Hence, building an implementation of formal models in a way that ensures DEVS formalism correctness is not easy. In this paper, we improve the interplay of abstraction (i.e., formal specification) and concreteness (i.e., programming code implementation) in advancing the theory and practice of DEVS using a specific-designed metamodel. The main contribution is a novel conceptualization of classic DEVS with ports founded on existing approaches but that also includes new improved elements related to the definition of atomic models. That is, our metamodel includes all the concepts and relationships needed to define the formal specification of DEVS atomic models. This allows us to define instances of our conceptualization that comply with the DEVS formal specification. To instantiate our metamodel, we propose a computer-aided environment that has been developed using the Eclipse Modeling Project. As an example, we show how our metamodel can be used to define the classic “switch” model. As a conclusion, we discuss how the final metamodel can be used to support interoperability with DEVS simulation tools.

Formal and Automatic Security Policy Enforcement on Android Applications by Rewriting1

With the wide variety of applications offered by Android, this system has been able to dominate the smartphone market. These applications provide all kinds of features and services that have become highly requested and welcomed by users. Besides, these applications represent risky vehicles for malware on Android devices. In this paper, we propose a novel formal technique to enforce the security of Android applications. We start off with an untrusted Android application and a security policy, and we end up in a new version of the application that behaves according to the policy. To ensure the correctness of results, we use formal methods in each step of the process, either in the system and the security policy specification or in the enforcement technique itself. The target application is reverse-engineered to its assembly-like code, Smali. An executable semantics called k-Smali was defined for this code using a language definitional framework, called k Framework. Security policies are specified in LTL-logic. The enforcement step consists of integrating the LTL formula in the k-Smali program using rewriting. It aims to rewrite the system specification automatically so that it satisfies the requested formula.

Simulation of a Fine Dust Value-Based False Data Detection System to Improve Security In WSN-Based Air Purification IoT

Fine dust refers to harmful substances floating in the air. It is divided into PM 2.5 and PM 10, and has the characteristic that the particles are small enough to be invisible to the naked eye. When fine dust enters a room, it can enter the human body through the bronchi and cause lung or respiratory diseases. To solve the health problems caused by fine dust, research and development about various air purification systems are progressing. In this paper, we introduce a Wireless Sensor Networks (WSNs)-based Internet of Things (IoT) air purification system. This WSNs-based IoT air purification system refers to a system in which an IoT air purifier and a window are automatically controlled based on fine dust values detected by sensor nodes. Therefore, because it is important to maintain the integrity of the fine dust values, SSL/TLS, an encryption protocol, is applied to this system. However, the existing SSL/TLS has a problem in which, if an attacker attempts a false data injection attack, the symmetric key itself used to encrypt and decrypt the data is stolen, so it cannot be detected. To solve this problem, in this paper we propose a Discrete Event System Specification (DEVS) model based on Data Calibration that verifies whether the fine dust values detected by sensor nodes and an IoT air purifier is within a preset error range. If the fine dust value is not within the preset error range, it is detected as false data, filtered, and not stored in the database. Because this proposed scheme verifies the integrity of the fine dust values, it not only raises the accuracy of collected sensing data, but also prevents abnormal operation of an IoT air purifier and a window in advance. Therefore, the security of the WSNs-based IoT air purification system is improved.

A Taxonomy for Model-Based Systems Engineering

In this paper, we define Model Based Systems Engineering (MBSE) as a set of different approaches which vary in scope and in purpose, as opposed to defining it as a monolithic concept. To do so, we inductively extract common themes from papers proposing new MBSE methods based on the type of Systems Engineering (SE) artifacts produced and the expected benefits of MBSE implementation. These themes are then validated against the experiences depicted in a second set of papers evaluating the deployment of MBSE methods in practice. We propose a taxonomy for MBSE which identifies three main categories: system specification repositories, system execution models, and design automation models. The proposed categories map well onto common discussions of the nature of the SE activity, in that the first is employed in the management of system development processes and the second in the understanding of system performance and emergent properties. The third category is almost exclusively discussed in an academic context and is therefore more difficult to relate to SE practice, but its features are clearly distinct from the other two. The proposed taxonomy clarifies what MBSE is and what it can be, therefore helping focus research on the issues that still prevent MBSE practice from living up to expectations.

From ERL to MBZIRC: Development of An Aerial-Ground Robotic Team for Search and Rescue

This chapter describes the efforts of the LARICS team in the 2019 European Robotics League (ERL) Emergency Robots and the 2020 Mohamed Bin Zayed International Robotics Challenge (MBZIRC) robotics competitions. We focus on the implementation of hardware and software modules that enable the deployment of aerial-ground robotic teams in unstructured environments for joint missions. In addition to the overall system specification, we outline the main algorithms for operation in such conditions: autonomous exploration of unknown environments and detection of objects of interest. Analysis of the results shows the success of the developed system in the competition arena of two of the largest outdoor robotics challenges. Throughout the chapter, we highlight the evolution of the robotic system based on the experience gained in the ERL competition. We conclude the chapter with key findings and additional improvement ideas to advance the state of the art in search and rescue applications of heterogeneous robotic teams.