Formal verification of cyber-physical systems (CPS) is challenging because it has to consider real-time and concurrency aspects that are often absent in ordinary software. Moreover, the software in CPS is often complex and low-level, making it hard to assure that a formal model of the system used for verification is a faithful representation of the actual implementation, which can undermine the value of a verification result. To address this problem, we propose a methodology for building verifiable CPS based on the principle that a formal model of the software can be derived
Verification of Cyberphysical Systems
The value of verification of cyberphysical systems depends on the relationship between the state of the software and the state of the physical system. This relationship can be complex because of the real-time nature and different timelines of the physical plant, the sensors and actuators, and the software that is almost always concurrent and distributed. In this paper, we study different ways to construct a transition system model for the distributed and concurrent software components of a CPS. The purpose of the transition system model is to enable model checking, an established and widely used verification technique. We describe a logical-time-based transition system model, which is commonly used for verifying programs written in synchronous languages, and derive the conditions under which such a model faithfully reflects physical states. When these conditions are not met (a common situation), a finer-grained event-based transition system model may be required. We propose an approach for formal verification of cyberphysical systems using Lingua Franca, a language designed for programming cyberphysical systems, and Rebeca, an actor-based language designed for model checking distributed event-driven systems. We focus on the cyber part and model a faithful interface to the physical part. Our method relies on the assumption that the alignment of different timelines during the execution of the system is the responsibility of the underlying platforms. We make those assumptions explicit and clear.
more »
« less
- Award ID(s):
- 1836601
- NSF-PAR ID:
- 10189436
- Date Published:
- Journal Name:
- Mathematics
- Volume:
- 8
- Issue:
- 7
- ISSN:
- 2227-7390
- Page Range / eLocation ID:
- 1068
- Format(s):
- Medium: X
- Sponsoring Org:
- National Science Foundation
More Like this
-
more » « less
automatically from its implementation. Our approach requires that the system implementation is specified inLingua Franca (LF), a polyglot coordination language tailored for real-time, concurrent CPS, which we made amenable to the specification of safety properties via annotations in the code. The program structure and the deterministic semantics of LF enable automatic construction of formal axiomatic models directly from LF programs. The generated models are automatically checked using Bounded Model Checking (BMC) by the verification engineUclid5 using theZ3 SMT solver. The proposed technique enables checking a well-defined fragment of Safety Metric Temporal Logic (Safety MTL) formulas. To ensure the completeness of BMC, we present a method to derive an upper bound on the completeness threshold of an axiomatic model based on the semantics of LF. We implement our approach in the LF Verifier and evaluate it using a benchmark suite with 22 programs sampled from real-life applications and benchmarks for Erlang, Lustre, actor-oriented languages, and RTOSes. The LF Verifier correctly checks 21 out of 22 programs automatically. -
This research paper describes the development of a critical incident-centered analysis methodology based on Schlossberg’s Transition Theory to explore transitions experienced by engineering education researchers as they begin new faculty positions. Understanding the transition experiences of scholars aiming to impact change within engineering education is important for identifying approaches to support the sustained success of these scholars at their institutions and within engineering education more broadly. To date, efforts to better prepare future faculty for academic roles have primarily focused on preparing them to be independent researchers, to teach undergraduate courses, and to support their ability to advance their career. Research of early career faculty is similarly limited in scope, focusing mostly on new faculty at research-exclusive universities or on faculty member’s teaching and research practices. To address this gap in the literature, our research team is examining the role of institutional context on the agency of early career engineering education faculty as it relates to facilitating change. As part of this larger project, the focus of this paper is on the integration of critical incident techniques and Schlossberg’s Transition Theory to create “incident timelines” that explore the transition of early career engineering education researchers into new faculty positions. Our paper will illustrate how this integration provided an effective methodology to: 1) explore a diverse set of transitions into faculty positions, 2) identify critical events that impact these transitions, 3) isolate strategies that supported the faculty members in different aspects of their transitions, and 4) examine connections between events and strategies over time and across faculty members’ transitions. Transition Theory provides a lens to explore how individuals identify and adapt based on transitions in their lives. An individual’s transition, according to Schlossberg, tends to include three phases: moving in, moving through, and moving out. Over the course of those phases, the individual’s experiences are influenced by the context of the transition, the characteristics of the individual such as their motivations and beliefs, the extent to which they have support, and the strategies they utilize. Given the complexity of a transition into a faculty position, it was necessary to determine the extent to which particular events and the relationship between events impacted a new faculty member’s experience. To accomplish this, we integrated a critical incident analysis to specifically investigate individual events that were considered significant to the overall transition leading to the development of an incident timeline. We applied our approach to monthly reflections of six new engineering faculty members from diverse institutional contexts who identify as engineering education researchers. The monthly reflections asked each participant to provide their impressions of the faculty role, in what ways they felt like a faculty member, and in what ways they did not. Through an iterative data analysis process, we developed initial incident timelines for each participant’s transition. Follow-up interviews with the participants allowed us to explore each event in more detail and provided an opportunity for reflection-on-action by the participant. These incidents were then further explored to distinguish strategies used and support received. Finally, we examined connections between events and strategies over time to identify overarching themes common to these types of faculty transitions. In this methods paper, we will demonstrate the usefulness of this variation of the critical incident approach for exploring complex professional transitions by highlighting the details of our incident timeline analysis.more » « less
-
This research paper describes the development of a critical incident-centered analysis methodology based on Schlossberg’s Transition Theory to explore transitions experienced by engineering education researchers as they begin new faculty positions. Understanding the transition experiences of scholars aiming to impact change within engineering education is important for identifying approaches to support the sustained success of these scholars at their institutions and within engineering education more broadly. To date, efforts to better prepare future faculty for academic roles have primarily focused on preparing them to be independent researchers, to teach undergraduate courses, and to support their ability to advance their career. Research of early career faculty is similarly limited in scope, focusing mostly on new faculty at research-exclusive universities or on faculty member’s teaching and research practices. To address this gap in the literature, our research team is examining the role of institutional context on the agency of early career engineering education faculty as it relates to facilitating change. As part of this larger project, the focus of this paper is on the integration of critical incident techniques and Schlossberg’s Transition Theory to create “incident timelines” that explore the transition of early career engineering education researchers into new faculty positions. Our paper will illustrate how this integration provided an effective methodology to: 1) explore a diverse set of transitions into faculty positions, 2) identify critical events that impact these transitions, 3) isolate strategies that supported the faculty members in different aspects of their transitions, and 4) examine connections between events and strategies over time and across faculty members’ transitions. Transition Theory provides a lens to explore how individuals identify and adapt based on transitions in their lives. An individual’s transition, according to Schlossberg, tends to include three phases: moving in, moving through, and moving out. Over the course of those phases, the individual’s experiences are influenced by the context of the transition, the characteristics of the individual such as their motivations and beliefs, the extent to which they have support, and the strategies they utilize. Given the complexity of a transition into a faculty position, it was necessary to determine the extent to which particular events and the relationship between events impacted a new faculty member’s experience. To accomplish this, we integrated a critical incident analysis to specifically investigate individual events that were considered significant to the overall transition leading to the development of an incident timeline. We applied our approach to monthly reflections of six new engineering faculty members from diverse institutional contexts who identify as engineering education researchers. The monthly reflections asked each participant to provide their impressions of the faculty role, in what ways they felt like a faculty member, and in what ways they did not. Through an iterative data analysis process, we developed initial incident timelines for each participant’s transition. Follow-up interviews with the participants allowed us to explore each event in more detail and provided an opportunity for reflection-on-action by the participant. These incidents were then further explored to distinguish strategies used and support received. Finally, we examined connections between events and strategies over time to identify overarching themes common to these types of faculty transitions. In this methods paper, we will demonstrate the usefulness of this variation of the critical incident approach for exploring complex professional transitions by highlighting the details of our incident timeline analysis.more » « less
-
null (Ed.)Background Mobile health technology has demonstrated the ability of smartphone apps and sensors to collect data pertaining to patient activity, behavior, and cognition. It also offers the opportunity to understand how everyday passive mobile metrics such as battery life and screen time relate to mental health outcomes through continuous sensing. Impulsivity is an underlying factor in numerous physical and mental health problems. However, few studies have been designed to help us understand how mobile sensors and self-report data can improve our understanding of impulsive behavior. Objective The objective of this study was to explore the feasibility of using mobile sensor data to detect and monitor self-reported state impulsivity and impulsive behavior passively via a cross-platform mobile sensing application. Methods We enrolled 26 participants who were part of a larger study of impulsivity to take part in a real-world, continuous mobile sensing study over 21 days on both Apple operating system (iOS) and Android platforms. The mobile sensing system (mPulse) collected data from call logs, battery charging, and screen checking. To validate the model, we used mobile sensing features to predict common self-reported impulsivity traits, objective mobile behavioral and cognitive measures, and ecological momentary assessment (EMA) of state impulsivity and constructs related to impulsive behavior (ie, risk-taking, attention, and affect). Results Overall, the findings suggested that passive measures of mobile phone use such as call logs, battery charging, and screen checking can predict different facets of trait and state impulsivity and impulsive behavior. For impulsivity traits, the models significantly explained variance in sensation seeking, planning, and lack of perseverance traits but failed to explain motor, urgency, lack of premeditation, and attention traits. Passive sensing features from call logs, battery charging, and screen checking were particularly useful in explaining and predicting trait-based sensation seeking. On a daily level, the model successfully predicted objective behavioral measures such as present bias in delay discounting tasks, commission and omission errors in a cognitive attention task, and total gains in a risk-taking task. Our models also predicted daily EMA questions on positivity, stress, productivity, healthiness, and emotion and affect. Perhaps most intriguingly, the model failed to predict daily EMA designed to measure previous-day impulsivity using face-valid questions. Conclusions The study demonstrated the potential for developing trait and state impulsivity phenotypes and detecting impulsive behavior from everyday mobile phone sensors. Limitations of the current research and suggestions for building more precise passive sensing models are discussed. Trial Registration ClinicalTrials.gov NCT03006653; https://clinicaltrials.gov/ct2/show/NCT03006653more » « less
-
Reasoning about memory aliasing and mutation in software verification is a hard problem. This is especially true for systems using SMT-based automated theorem provers. Memory reasoning in SMT verification typically requires a nontrivial amount of manual effort to specify heap invariants, as well as extensive alias reasoning from the SMT solver. In this paper, we present a hybrid approach that combines linear types with SMT-based verification for memory reasoning. We integrate linear types into Dafny, a verification language with an SMT backend, and show that the two approaches complement each other. By separating memory reasoning from verification conditions, linear types reduce the SMT solving time. At the same time, the expressiveness of SMT queries extends the flexibility of the linear type system. In particular, it allows our linear type system to easily and correctly mix linear and nonlinear data in novel ways, encapsulating linear data inside nonlinear data and vice-versa. We formalize the core of our extensions, prove soundness, and provide algorithms for linear type checking. We evaluate our approach by converting the implementation of a verified storage system (about 24K lines of code and proof) written in Dafny, to use our extended Dafny. The resulting system uses linear types for 91% of the code and SMT-based heap reasoning for the remaining 9%. We show that the converted system has 28% fewer lines of proofs and 30% shorter verification time overall. We discuss the development overhead in the original system due to SMT-based heap reasoning and highlight the improved developer experience when using linear types.more » « less
- Free Publicly Accessible Full Text
-
Accepted Manuscript1.0
- Journal Article:
- https://doi.org/10.3390/math8071068
