skip to main content

Title: 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 more » 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. « less
Authors:
; ;
Award ID(s):
1836601
Publication Date:
NSF-PAR ID:
10189436
Journal Name:
Mathematics
Volume:
8
Issue:
7
Page Range or eLocation-ID:
1068
ISSN:
2227-7390
Sponsoring Org:
National Science Foundation
More Like this
  1. 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. Ourmore »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.« less
  2. 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. Ourmore »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.« less
  3. 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 constructsmore »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/NCT03006653« less
  4. 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 typesmore »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.« less
  5. Modern physical systems deploy large numbers of sensors to record at different time-stamps the status of different systems components via measurements such as temperature, pressure, speed, but also the component's categorical state. Depending on the measurement values, there are two kinds of sequences: continuous and discrete. For continuous sequences, there is a host of state-of-the-art algorithms for anomaly detection based on time-series analysis, but there is a lack of effective methodologies that are tailored specifically to discrete event sequences. This paper proposes an analytics framework for discrete event sequences for knowledge discovery and anomaly detection. During the training phase, the framework extracts pairwise relationships among discrete event sequences using a neural machine translation model by viewing each discrete event sequence as a "natural language". The relationship between sequences is quantified by how well one discrete event sequence is "translated" into another sequence. These pairwise relationships among sequences are aggregated into a multivariate relationship graph that clusters the structural knowledge of the underlying system and essentially discovers the hidden relationships among discrete sequences. This graph quantifies system behavior during normal operation. During testing, if one or more pairwise relationships are violated, an anomaly is detected. The proposed framework is evaluated onmore »two real-world datasets: a proprietary dataset collected from a physical plant where it is shown to be effective in extracting sensor pairwise relationships for knowledge discovery and anomaly detection, and a public hard disk drive dataset where its ability to effectively predict upcoming disk failures is illustrated.« less