A Formal Verification of a Reputation Multi-Factor Authentication Mechanism for Constrained Devices and Low-Power Wide-Area Network Using Temporal Logic.

There are many security challenges in IoT, especially related to the authentication of restricted devices in long-distance and low-throughput networks. Problems such as impersonation, privacy issues, and excessive battery usage are some of the existing problems evaluated through the threat modeling of this work. A formal assessment of security solutions for their compliance in addressing such threats is desirable. Although several works address the verification of security protocols, verifying the security of components and their non-locking has been little explored. This work proposes to analyze the design-time security of the components of a multi-factor authentication mechanism with a reputation regarding security requirements that go beyond encryption or secrecy in data transmission. As a result, it was observed through temporal logic that the mechanism is deadlock-free and meets the requirements established in this work. Although it is not a work aimed at modeling the security mechanism, this document provides the necessary details for a better understanding of the mechanism and, consequently, the process of formal verification of its security properties.

Broadcast Propagation Time in SpaceFibre Networks with Various Types of Spatial Redundancy.

Various methods of spatial redundancy can be used in local networks based on the SpaceFibre standard for fault mitigation of network hardware and physical communication channels. Usually, a network developer chooses the method of spatial redundancy according to the number of failures that have to be mitigated, the time required for restoring the normal operation of the network, required overheads and hardware costs. The use of different spatial redundancy mechanisms can cause changes in the structure of the links between network nodes, in case of failure and subsequent mitigation. In turn, this may cause changes in the broadcast transmission paths and the temporal characteristics of their delivery from the source to the receivers. This article focuses on the change in the propagation time of broadcasts in SpaceFibre networks with spatial redundancy. Broadcast propagation rules significantly differ from data-packet propagation rules. Broadcast distribution time is very important for many applications, because broadcasts are generally used to send urgent messages, in particular for time synchronization. Various formal methods have been used to evaluate the propagation characteristics of the broadcast. A method for estimating broadcast propagation time along the shortest routes is proposed. In addition, we provide a formal method to estimate the number of failures, which occurred in the network during the broadcast propagation. This method is based on timed Petri nets; one of its features is the ability to calculate broadcast transmission delays. In addition, as an alternative solution, we propose a method for estimating delays based on time automata theory.

Bounded Model Checking for Metric Temporal Logic Properties of Timed Automata with Digital Clocks.

Metric temporal logic (MTL) is a popular real-time extension of linear temporal logic (LTL). This paper presents a new simple SAT-based bounded model-checking (SAT-BMC) method for MTL interpreted over discrete infinite timed models generated by discrete timed automata with digital clocks. We show a new translation of the existential part of MTL to the existential part of linear temporal logic with a new set of atomic propositions and present the details of the new translation. We compare the new method's advantages to the old method based on a translation of the hard reset LTL (HLTL). Our method does not need new clocks or new transitions. It uses only one path and requires a smaller number of propositional variables and clauses than the HLTL-based method. We also implemented the new method, and as a case study, we applied the technique to analyze several systems. We support the theoretical description with the experimental results demonstrating the method's efficiency.

Modeling and Verification of Asynchronous Systems Using Timed Integrated Model of Distributed Systems.

In modern computer systems, distributed systems play an increasingly important role, and modeling and verification are crucial in their development. The specificity of many systems requires taking this into account in real time, as time dependencies significantly affect the system's behavior, when achieving the goals of its processes or with adverse phenomena such as deadlocks. The natural features of distributed systems include the asynchrony of actions and communication, the autonomy of nodes, and the locality of behavior, i.e., independence from any global or non-local features. Most modeling formalisms are derived from parallel centralized systems, in which the behavior of components depends on the global state or the simultaneous achievement of certain states by components. This approach is unrealistic for distributed systems. This article presents the formalism of a timed integrated model of distributed systems that supports all of the mentioned features. The formalism is based on the relation between the states of the distributed nodes and the messages of distributed computations, called agents. This relation creates system actions. A specification in this formalism can be translated into timed automata, the most popular formalism for specifying and verifying timed parallel systems. The translation rules ensure that the semantics of T-IMDS and timed automata are consistent, allowing use of the Uppaal validator for system verification. The development of general formulas for checking the deadlock freedom and termination efficiency allows for automated verification, without learning temporal logics and time-dependent formulas. An important and rare feature is the finding of partial deadlocks, because in a distributed system a common situation occurs in which some nodes/processes are deadlocked, while others work. Examples of checking timed distributed systems are included.

A methodology for evaluating tooth wear monitoring using timed automata modelling.

OBJECTIVES: Tooth wear is a multifactorial condition leading to the loss of dental hard tissues. A counselling/monitoring protocol is of importance in order to keep that loss as limited as possible. Since many factors are involved and a time span of decades is included, research to disentangle all these processes in patients is difficult. Instead, a modelling technique was used that is able to deal with time, costs and probabilistic and stochastic information. The aim was to shed light on the question: does a yearly or a once-in-five-years counselling/monitoring protocol yield better outcome measures? METHODS: A so-called timed automata model was adopted, analysed with the tool UPPAAL. To our knowledge, this is the first time that formal modelling is applied in dentistry. In this article, a UPPAAL model for the evaluation of tooth wear is described. RESULTS: Using the UPPAAL model, it was calculated that with a yearly counselling/monitoring protocol the severity of tooth wear at age 74, the total costs per person and the number of restorative treatments were less, and the number of so-called "good years" was higher. CONCLUSIONS: With the use of the UPPAAL model, it may be concluded that a yearly counselling/monitoring protocol can yield better outcome measures. CLINICAL SIGNIFICANCE: Regarding dentistry in general and tooth wear in particular, with the use of a timed automata model in UPPAAL, actual research questions can be answered, factors of influence in a multifactorial condition like tooth wear can be clarified, and future research topics can be determined.

Comparison of Timed Automata with Discrete Event Simulation for Modeling of Biomarker-Based Treatment Decisions: An Illustration for Metastatic Castration-Resistant Prostate Cancer.

BACKGROUND: With the advent of personalized medicine, the field of health economic modeling is being challenged and the use of patient-level dynamic modeling techniques might be required. OBJECTIVES: To illustrate the usability of two such techniques, timed automata (TA) and discrete event simulation (DES), for modeling personalized treatment decisions. METHODS: An early health technology assessment on the use of circulating tumor cells, compared with prostate-specific antigen and bone scintigraphy, to inform treatment decisions in metastatic castration-resistant prostate cancer was performed. Both modeling techniques were assessed quantitatively, in terms of intermediate outcomes (e.g., overtreatment) and health economic outcomes (e.g., net monetary benefit). Qualitatively, among others, model structure, agent interactions, data management (i.e., importing and exporting data), and model transparency were assessed. RESULTS: Both models yielded realistic and similar intermediate and health economic outcomes. Overtreatment was reduced by 6.99 and 7.02 weeks by applying circulating tumor cell as a response marker at a net monetary benefit of -€1033 and -€1104 for the TA model and the DES model, respectively. Software-specific differences were observed regarding data management features and the support for statistical distributions, which were considered better for the DES software. Regarding method-specific differences, interactions were modeled more straightforward using TA, benefiting from its compositional model structure. CONCLUSIONS: Both techniques prove suitable for modeling personalized treatment decisions, although DES would be preferred given the current software-specific limitations of TA. When these limitations are resolved, TA would be an interesting modeling alternative if interactions are key or its compositional structure is useful to manage multi-agent complex problems.

Dynamic Data Structures for Timed Automata Acceptance.

We study a variant of the classical membership problem in automata theory, which consists of deciding whether a given input word is accepted by a given automaton. We do so through the lenses of parameterized dynamic data structures: we assume that the automaton is fixed and its size is the parameter, while the input word is revealed as in a stream, one symbol at a time following the natural order on positions. The goal is to design a dynamic data structure that can be efficiently updated upon revealing the next symbol, while maintaining the answer to the query on whether the word consisting of symbols revealed so far is accepted by the automaton. We provide complexity bounds for this dynamic acceptance problem for timed automata that process symbols interleaved with time spans. The main contribution is a dynamic data structure that maintains acceptance of a fixed one-clock timed automaton  A with amortized update time  2 O ( | A | ) per input symbol.

Formal Verification of Real-Time Autonomous Robots: An Interdisciplinary Approach.

Due to the severe consequences of their possible failure, robotic systems must be rigorously verified as to guarantee that their behavior is correct and safe. Such verification, carried out on a model, needs to cover various behavioral properties (e.g., safety and liveness), but also, given the timing constraints of robotic missions, real-time properties (e.g., schedulability and bounded response). In addition, in order to obtain valid and useful verification results, the model must faithfully represent the underlying robotic system and should therefore take into account all possible behaviors of the robotic software under the actual hardware and OS constraints (e.g., the scheduling policy and the number of cores). These requirements put the rigorous verification of robotic systems at the intersection of at least three communities: the robotic community, the formal methods community, and the real-time systems community. Verifying robotic systems is thus a complex, interdisciplinary task that involves a number of disciplines/techniques (e.g., model checking, schedulability analysis, component-based design) and faces a number of challenges (e.g., formalization, automation, scalability). For instance, the use of formal verification (formal methods community) is hindered by the state-space explosion problem, whereas schedulability analysis (real-time systems) is not suitable for behavioral properties. Moreover, current real-time implementations of robotic software are limited in terms of predictability and efficiency, leading to, e.g., unnecessary latencies. This is flagrant, in particular, at the level of locking protocols in robotic software. Such situation may benefit from major theoretical and practical findings of the real-time systems community. In this paper, we propose an interdisciplinary approach that, by joining forces of the different communities, provides a scalable and unified means to efficiently implement and rigorously verify real-time robots. First, we propose a scalable two-step verification solution that combines formal methods and schedulability analysis to verify both behavioral and real-time properties. Second, we devise a new multi-resource locking mechanism that is efficient, predictable, and suitable for real-time robots and show how it improves the latter's real-time behavior. In both cases, we show, using a real drone example, how our approach compares favorably to that in the literature. This paper is a major extension of the RTCSA 2020 publication "A Two-Step Hybrid Approach for Verifying Real-Time Robotic Systems."

Modeling Diagnostic Strategies to Manage Toxic Adverse Events following Cancer Immunotherapy.

BACKGROUND: Although immunotherapy (IMT) provides significant survival benefits in selected patients, approximately 10% of patients experience (serious) immune-related adverse events (irAEs). The early detection of adverse events will prevent irAEs from progressing to severe stages, and routine testing for irAEs has become common practice. Because a positive test outcome might indicate a clinically manifesting irAE that requires treatment to (temporarily) discontinue, the occurrence of false-positive test outcomes is expected to negatively affect treatment outcomes. This study explores how the UPPAAL modeling environment can be used to assess the impact of test accuracy (i.e., test sensitivity and specificity), on the probability of patients entering palliative care within 11 IMT cycles. METHODS: A timed automata-based model was constructed using real-world data and expert consultation. Model calibration was performed using data from 248 non-small-cell lung cancer patients treated with nivolumab. A scenario analysis was performed to evaluate the effect of changes in test accuracy on the probability of patients transitioning to palliative care. RESULTS: The constructed model was used to estimate the cumulative probabilities for the patients' transition to palliative care, which were found to match real-world clinical observations after model calibration. The scenario analysis showed that the specificity of laboratory tests for routine monitoring has a strong effect on the probability of patients transitioning to palliative care, whereas the effect of test sensitivity was limited. CONCLUSION: We have obtained interesting insights by simulating a care pathway and disease progression using UPPAAL. The scenario analysis indicates that an increase in test specificity results in decreased discontinuation of treatment due to suspicion of irAEs, through a reduction of false-positive test outcomes.

Exact acceleration of complex real-time model checking based on overlapping cycle.

When real-time systems are modeled as timed automata, different time scales may lead to substantial fragmentation of the symbolic state space. Exact acceleration solves the fragmentation problem without changing system reachability. The relatively mature technology of exact acceleration has been used with an appended cycle or a parking cycle, which can be applied to the calculation of a single acceleratable cycle model. Using these two technologies to develop a complex real-time model requires additional states and consumes a large amount of time cost, thereby influencing acceleration efficiency. In this paper, a complex real-time exact acceleration method based on an overlapping cycle is proposed, which is an application scenario extension of the parking-cycle technique. By comprehensively analyzing the accelerating impacts of multiple acceleratable cycles, it is only necessary to add a single overlapping period with a fixed length without relying on the windows of acceleratable cycles. Experimental results show that the proposed timed automaton model is simple and effectively decreases the time costs of exact acceleration. For the complex real-time system model, the method based on an overlapping cycle can accelerate the large scale and concurrent states which cannot be solved by the original exact acceleration theory.

Modelling with ANIMO: between fuzzy logic and differential equations.

BACKGROUND: Computational support is essential in order to reason on the dynamics of biological systems. We have developed the software tool ANIMO (Analysis of Networks with Interactive MOdeling) to provide such computational support and allow insight into the complex networks of signaling events occurring in living cells. ANIMO makes use of timed automata as an underlying model, thereby enabling analysis techniques from computer science like model checking. Biology experts are able to use ANIMO via a user interface specifically tailored for biological applications. In this paper we compare the use of ANIMO with some established formalisms on two case studies. RESULTS: ANIMO is a powerful and user-friendly tool that can compete with existing continuous and discrete paradigms. We show this by presenting ANIMO models for two case studies: Drosophila melanogaster circadian clock, and signal transduction events downstream of TNF α and EGF in HT-29 human colon carcinoma cells. The models were originally developed with ODEs and fuzzy logic, respectively. CONCLUSIONS: Two biological case studies that have been modeled with respectively ODE and fuzzy logic models can be conveniently modeled using ANIMO. The ANIMO models require less parameters than ODEs and are more precise than fuzzy logic. For this reason we position the modelling paradigm of ANIMO between ODEs and fuzzy logic.