Search for: All records

Modern cyber-physical systems-of-systems (CPSoS) operate in complex systems-of-systems that must seamlessly work together to control safety- or mission-critical functions. Linear Temporal Logic (LTL) and Mission-time Linear Temporal logic (MLTL) intuitively express CPSoS requirements for automated system verification and validation. However, both LTL and MLTL presume that all signals populating the variables in a formula are sampled over the same rate and type (e.g., time or distance), and agree on a standard “time” step. Formal verification of cyber-physical systems-of-systems needs validate-able requirements expressed over (sub-)system signals of different types, such as signals sampled at different timescales, distances, or levels of abstraction, expressed in the same formula. Previous works developed more expressive logics to account for types (e.g., timescales) by sacrificing the intuitive simplicity of LTL. However, a legible direct one-to-one correspondence between a verbal and formal specification will ease validation, reduce bugs, increase productivity, and linearize the workflow from a project’s conception to actualization. Validation includes both transparency for human interpretation, and tractability for automated reasoning, as CPSoS often run on resource-limited embedded systems. To address these challenges, we introduced Mission-time Linear Temporal Logic Multi-type (Hariharan et al., Numerical Software Verification Workshop, 2022), a logic building on MLTL. MLTLM enables writing formal requirements over finite input signals (e.g., sensor signals and local computations) of different types, while maintaining the same simplicity as LTL and MLTL. Furthermore, MLTLM maintains a direct correspondence between a verbal requirement and its corresponding formal specification. Additionally, reasoning a formal specification in the intended type (e.g., hourly for an hourly rate, and per second for a seconds rate) will use significantly less memory in resource-constrained hardware. This article extends the previous work with (1) many illustrated examples on types (e.g., time and space) expressed in the same specification, (2) proofs omitted for space in the workshop version, (3) proofs of succinctness of MLTLM compared to MLTL, and (4) a minimal translation to MLTL of optimal length. 

Autonomous cyber-physical systems must be able to operate safely in a wide range of complex environments. To ensure safety without limiting mitigation options, these systems require detection of safety violations by mitigation trigger deadlines. As a result of these system’s complex environments, multimodal prediction is often required. For example, an autonomous vehicle (AV) operates in complex traffic scenes that result in any given vehicle having the ability to exhibit several plausible future behavior modes (e.g., stop, merge, turn, etc.); therefore, to ensure collision avoidance, an AV must be able to predict the possible multimodal behaviors of nearby vehicles. In previous work, model predictive runtime verification (MPRV) successfully detected future violations by a given deadline, but MPRV only considers a single mode of prediction (i.e., unimodal prediction). We design multimodal model predictive runtime verification (MMPRV) to extend MPRV to consider multiple modes of prediction, and we introduce Predictive Mission-Time Linear Temporal Logic (PMLTL) as an extension of MLTL to support the evaluation of probabilistic multimodal predictions. We examine the correctness and real-time feasibility of MMPRV through two AV case studies where MMPRV utilizes (1) a physics-based multimodal predictor on the F1Tenth autonomous racing vehicle and (2) current state-of-the-art deep neural network multimodal predictors trained and evaluated on the Argoverse motion forecasting dataset. We found that the ability to meet real-time requirements was a challenge for the latter, especially when targeting an embedded computing platform. 

This Research-to-Practice Full Paper describes the implementation of integrated reflective activities in two computer engineering courses. Reflective activities contribute to student learning and professional development. Instructional team members have been examining the need and opportunities to deepen learning by integrating reflective activities into problem-solving experiences. We implemented reflective activities using a coordinated framework for a modified Kolbian cycle. The framework consists of reflection-for-action, reflection-in-action, reflection-on-action, and composted reflections. Reflection-for-action takes place before the experience and involves thinking about and planning future actions. Reflection-in-action takes place during the experience while actively problem-solving. Reflection-on-action takes place after the problem-solving experience. Composting involves revisiting past experiences and reflections to inform future planning. We describe the reflective activities in the context of the coordinated framework, including strategies to support reflection and increase the likelihood of engagement and success. We conclude with an analysis of the activities using the CPREE framework for reflection pathways. 

This Research-to-Practice Full Paper presents the redesign of a course project to promote student professional formation in engineering in the Electrical and Computer Engineering Department at Iowa State University. This is part of a larger effort to redesign core courses in the sophomore and junior years through a collaborative instructional model and pedagogical approaches that promote professional formation. A required sophomore course on embedded computer systems has been assessed and revised over multiple semesters. The redesign of the project was initiated with the purpose of promoting student professional formation, interest, autonomy and innovation, and it was undertaken using a collaborative process. This paper describes the course, final project, redesign process, assessment, results and future work. Several conclusions from the research may be useful to other educators. A small change to the course project yielded positive effects in interest and autonomy and may influence longer term effects of the project. There was evidence of difference in engagement with the project. The difference observed was not only due to option selected by students but why students selected the option.