Add profile and tools to loonwerks website

_data/authors.yml

@@ -1,3 +1,4 @@
+A. Aurandt: <<a href="/people/alexis-aurandt.html">A. Aurandt</a>
 A. Gacek: <a href="/people/andrew-gacek.html">A. Gacek</a>
 J. Backes: <a href="/people/john-backes.html">J. Backes</a>
 D. Cofer: <a href="/people/darren-cofer.html">D. Cofer</a>

people/alexis-aurandt.html

@@ -0,0 +1,31 @@
+---
+layout: person
+fullname: Alexis Aurandt
+sort: Aurandt
+author_key: A. Aurandt
+position: Senior Engineer
+picture: /images/aurandt.jpg
+email: Alexis.Aurandt2@collins.com
+location: Pennsylvania
+---
+
+<p>
+Alexis Aurandt is a Senior Engineer in the Trusted Methods group within the Applied Research in the Applied 
+Research and Technology (ART) organization at Collins Aerospace. Her main areas of research are temporal logics,
+embedded systems, and runtime verification, particularly through contributions to the <a href="/tools/r2u2.html">R2U2</a> framework. 
+She is also involved in advancing verification and assurance methods for safety-critical aerospace systems, collaborating
+with both academic and industry partners to transition formal methods into practical engineering workflows through projects such as <a href="/tools/fret.html">FRET</a> and DARPA's
+<a href="/projects/matrics.html">MATRICS</a> and <a href="/projects/inspecta.html">INSPECTA</a> programs.
+
+<p>
+Dr. Aurandt received both her BS (2021) and her PhD (2025) in Computer Engineering from Iowa State University.
+Her published research during her Graduate studies includes the following:
+<ul>
+  <li><a href="https://link.springer.com/chapter/10.1007/978-3-031-06773-0_45">Runtime Verification Triggers Real-time, Autonomous Fault Recovery on the CySat-I</a></li>
+  <li><a href="https://link.springer.com/chapter/10.1007/978-3-031-42626-1_10">Model Predictive Runtime Verification for Cyber-Physical Systems with Real-time Deadlines</a></li>
+  <li><a href="https://link.springer.com/chapter/10.1007/978-3-031-68150-9_13">Multimodal Model Predictive Runtime Verification for Safety of Autonomous Cyber-Physical Systems</a></li>
+  <li><a href="https://link.springer.com/chapter/10.1007/978-3-031-93706-4_3">Towards a Safe, Verified Runtime Monitor for Embedded Systems: R2U2 in Embedded Rust</a></li>
+  <li><a href="https://ieeexplore.ieee.org/abstract/document/11378084">R2U2 Playground: Visualization of a Real-time, Temporal Logic Runtime Monitor</a></li>
+</ul>
+</p>
+

publications/aurandt2026nfm.html

@@ -5,6 +5,7 @@
 info: NASA Formal Methods symposium (NFM 2026), May 2026
 link: "/publications/pdf/aurandt2026nfm.pdf"
 date: 2026-05-05 00:00:00
+tools: [FRET, R2U2]
 ---
 
 The Realizable, Responsive, Unobtrusive Unit (R2U2) is a stream-based runtime monitoring framework that verifies a system’s adherence to a set of formal system requirements with minimal resource overhead, allowing for real-time, online monitoring on resource-constrained systems. Yet, a persisting challenge for deploying runtime monitors is eliciting formal specifications that accurately capture system requirements commonly expressed in ambiguous natural language; therefore, we employ NASA’s Formal Requirements Elicitation Tool (FRET) to configure R2U2 monitors from structured natural language requirements. We extend FRET to formalize requirements in Mission-time Linear Temporal Logic (MLTL) - the native specification logic of R2U2, and we provide 157 MLTL rewrite rules that reduce each of FRET’s MLTL formalizations by an average of 15 operators, or 36.05%, decreasing the resources necessary to monitor these requirements with R2U2. We also introduce a novel SMT-based proof technique for automatically proving the correctness of these rewrite rules.

tools/fret.html

@@ -0,0 +1,11 @@
+---
+layout: tool
+toolname: FRET
+summary: Formal Requirements Elicitation Tool
+sourcecode: "https://github.com/NASA-SW-VnV/fret/tree/v3.1.0"
+download: "https://github.com/NASA-SW-VnV/fret/releases/v3.1.0"
+---
+
+<p>
+The Formal Requirements Elictation Tool (FRET) is a framework for the elicitation, specification, formalization, and analysis of system requirements composed in a structed natural language known as FRETish. FRET is an open-source tool hosted by NASA.
+</p>

tools/r2u2.html

@@ -0,0 +1,11 @@
+---
+layout: tool
+toolname: R2U2
+summary: Realizable, Responsive, Unobtrusive Unit
+sourcecode: "https://github.com/R2U2/r2u2"
+download: "https://github.com/R2U2/r2u2/releases"
+---
+
+<p>
+The Realizable, Responsive, Unobtrusive Unit (R2U2) is a stream-based runtime verification framework based on Mission-time Linear Temporal Logic (MLTL) designed to monitor safety- or mission-critical systems with constrained computational resources. R2U2 provides a python-based front-end compiler (C2PO) with deployable realizations in both C and <a href="https://crates.io/crates/r2u2_core">embedded Rust</a>.  
+</p>