ISU Aerospace Engineering Alumni and Boeing CEO Dennis Muilenburg visited the department and met with many of the students and faculty.
He was joined by fellow ISU Aerospace Engineering Alumni and former CEO of Lockheed Martin Vance Coffman for a fascinating panel: “Perspectives on Aerospace Leadership.” More information, including the video, is available here.
Filed under News Features
PI Prof. Kristin Yvonne Rozier presented a poster on current grant “CAREER: Theoretical Foundations of the UAS in the NAS Problem (Unmanned Aerial Systems in the National Air Space)” at the 2016 NSF Cyber-Physical Systems Principal Investigators’ Meeting October 31-November 1, 2016. This seventh annual Cyber-Physical Systems (CPS) PI meeting gathered researchers and collaborators from around the world!
According to the NSF, “The CPS Principal Investigators’ Meeting provided a forum for a wide range of stakeholders in academia, industry, and Federal agencies to review new developments in CPS foundations, to identify new, emerging applications, and to discuss technology gaps and barriers. The program of the meeting included presentations about projects funded by NSF and other agencies, keynotes, panels, discussion groups, and poster & demonstration sessions.”
This year’s NSF CPS PI meeting was held at the Renaissance Arlington Capital View (RACV) Hotel located in the Crystal City Community of Arlington, Virginia at 2800 South Potomac Avenue, Arlington, Virginia 22202. The RACV is 0.9 miles from the Reagan Washington National Airport (DCA). Watching the planes land that will someday fly our research is an exciting experience!
Filed under Awards, Research Talks
Ph.D. Student Rohit Dureja presented a poster at Formal Methods in Computer-Aided Design (FMCAD’16) on “Comparative Safety Analysis of Wireless Communication Networks in Avionics.”
Abstract: Comparative Safety Analysis of Wireless Communication Networks in Avionics
Existing wired networks add weight and complexity to current aircraft design. To reduce weight of aircraft, it is essential to decrease the number of wired components and move them to wireless. However, migration of wired to wireless needs to be supported by a thorough analysis of the complexities and failure aspects of the two mediums. The wireless network needs to be at least as reliable and fault tolerant as the existing wired network. This paper proposes a formal framework for a comparative safety analysis of wired and wireless networks. Due to the plug-and-play nature of the framework, it is adaptable to a wide variety of network protocols. It facilitates identification of the minimum set of events that lead to system failure, and using quantified failure probabilities recommends fault tolerant mechanisms that increase system reliability. Designers can then compare candidates for wireless protocols among each other, as well as the wired network, and make informed design decisions.
Filed under Research Talks
Patrick Moosbrugger received the “Würdigungspreis” of the Federal Ministry of Science Research and Economy for his master thesis entitled “A Real-time, On-board System Health Management Unit for Unmanned Aerial Systems”. The thesis, done in cooperation with NASA Ames Research Center deals with runtime monitoring and diagnosis for unmanned aerial systems. The thesis is also related to Patricks work in the Josef Ressel Center for Verification of Embedded Computing Systems at TU Vien.
More information about this award is available in German here (https://www.technikum-wien.at/newsroom/news/wuerdigungspreis-fuer-patrick-moosbrugger) and here (http://wissenschaft.bmwfw.gv.at/index.php?id=3791).
Filed under Awards, News Features, Publication Highlights
NASA’s Space Technology Mission Directorate (STMD) announced today that the proposal by Prof. Kristin Yvonne Rozier entitled “Multi-Platform, Multi-Architecture Runtime Verification of Autonomous Space Systems” was selected for funding under the call for Verification and Validation of Autonomous Systems.
According to NASA: “The Early Career Faculty (ECF) component of the Space Technology Research Grants Program awards grants to accredited U.S. universities on behalf of outstanding faculty researchers early in their careers. ECF challenges early career faculty to examine the theoretical feasibility of ideas and approaches that are critical to making science, space travel, and exploration more effective, affordable, and sustainable. Awards result from successful proposals to the ECF Appendix to the SpaceTech-REDDI NASA Research Announcement. The ECF Appendix is expected to be released at least biannually and will feature specific topics. Awards are expected to be a maximum of three years in duration and the typical award amount is $200K/year.”
Abstract:
Autonomous systems are only capable of effective self-governing if they can reliably sense their own faults and respond to failures and uncertain environmental conditions. We propose to design a real-time, onboard runtime verification and system health management (SHM) framework called R2U2, to continuously monitor essential system components such as sensors, software, and hardware for detection and diagnosis of failures and violations of safety or performance rules during the mission of autonomous space systems, such as rovers, small satellites, or Unmanned Aerial Systems (UAS) flying in the skies of other planets. R2U2 is multi-platform and multi-architecture to address the requirements and capabilities of these embedded systems. R2U2 stands for Responsive, Realizable, Unobtrusive Unit; it is named after its three crucial properties that are currently absent from state-of-the-art SHM capabilities. Responsiveness means evaluating system health in real time, with provable timing and performance guarantees. Realizability involves being adaptable, extensible, and scalable to multiple platforms and architectures. Unobtrusiveness requires R2U2 to operate without altering crucial properties of the system: functionality, certifiability, timing, or tolerances for size, weight, power, telemetry bandwidth, software overhead. A full-scale version of R2U2, with options for hardware- and software-based implementations would have tremendous impact on the ability of autonomous space systems to perform real-time system-level reasoning about their health.
Congratulations to the seven fellow NASA ECF Award Winners: Necmiye Ozay (University Of Michigan), Seok Woo Lee (University of Connecticut), SungWoo Nam (University of Illinois at Urbana-Champaign), Sonia Chernova (Georgia Institute of Technology), Dimitra Panagou (University Of Michigan), Daniel Szafir (University Of Colorado, Boulder), and Stefanie Tellex (Brown University).
Filed under Awards, News Features
The Fields Institute for Research in Mathematical Sciences hosted an invitation-only Workshop on Theoretical Foundations of SAT Solving August 15-19, 2016. This workshop explored one of the most important problems in all of mathematics and computer science: the Boolean satisfiability (SAT) problem. The workshop focused on the state-of-the-art research developments in Boolean satisfiability, the quintessential NP-complete problem. While SAT is believed to be intractable in general, researchers have contributed dramatic developments in algorithmic techniques in solving SAT during the last two decades. Modern SAT solvers can now solve large real-world instances obtained from wide-ranging applications such as hardware and software verification, electronic design automation, artificial intelligence, bioinformatics, and operations research; these advances were featured in the workshop’s seminars, available online. The workshop was organized by eight of the most prominent researchers in SAT: Vijay Ganesh – University of Waterloo (Lead Organizer); Armin Biere – Johannes Kepler University; Sam Buss – University of California, San Diego; John Franco – University of Cincinatti; Holger Hoos – University of British Columbia; Jakob Nordström – KTH, Royal Institute of Technology; Alasdair Urquhart – University of Toronto; Moshe Vardi – Rice University.
The related topic of Linear Temporal Logic Satisfiability builds on advances in SAT in many ways. Professor Kristin Yvonne Rozier contributed a talk on Linear Temporal Logic Satisfiability Checking exploring this relationship with aerospace domain examples.
We have established LTL satisfiability checking as a sanity check: each system requirement, its negation, and the set of all requirements should be checked for satisfiability before being utilized for other tasks. We demonstrated that LTL satisfiability checking reduces to model checking, and developed new encodings that performed significantly, sometimes exponentially, better than was previously possible. Others then built on our work to create new stand-alone tools for LTL Satisfiability. However, the state of the art leaves many open questions for future applications of LTL satisfiability.
Slides for this presentation on Linear Temporal Logic Satisfiability Checking are available online.
Filed under Laboratory Collaborations, Research Talks
The National Science Foundation (NSF) Cyber-Physical Systems (CPS) Program announced today that the proposal by Prof. Kristin Yvonne Rozier entitled CAREER: Theoretical Foundations of the UAS in the NAS Problem (Unmanned Aerial Systems in the National Air Space) was selected for funding.
According to the NSF: “The Faculty Early Career Development (CAREER) Program is a Foundation-wide activity that offers the National Science Foundation’s most prestigious awards in support of junior faculty who exemplify the role of teacher-scholars through outstanding research, excellent education and the integration of education and research within the context of the mission of their organizations. Such activities should build a firm foundation for a lifetime of leadership in integrating education and research.”
The following is a quote from the NSF’s Program Description for the CAREER award:
“This premier program emphasizes the importance the Foundation places on the early development of academic careers dedicated to stimulating the discovery process in which the excitement of research is enhanced by inspired teaching and enthusiastic learning. Effective integration of research and education generates a synergy in which the process of discovery stimulates learning, and assures that the findings and methods of research and education are quickly and effectively communicated in a broader context and to a larger audience.
“The CAREER program embodies NSF’s commitment to encourage faculty and academic institutions to value and support the integration of research and education. Successful PIs will propose creative, integrative and effective research and education plans, developed within the context of the mission, goals, and resources of their organizations, while building a firm foundation for a lifetime of contributions to research, education and their integration.”
Abstract: Theoretical Foundations of the UAS in the NAS Problem
Due to their increasing use by civil and federal authorities and vast commercial and amateur applications, Unmanned Aerial Systems (UAS) will be introduced into the National Air Space (NAS); the question is only how this can be done safely. Today, NASA and the FAA are designing a new, (NextGen) automated air traffic control system for all aircraft, manned or unmanned. New algorithms and tools will need to be developed to enable computation of the complex questions inherent in designing such a system while proving adherence to rigorous safety standards. Researchers must develop the tools of formal analysis to be able to address the UAS in the NAS problem, reason about UAS integration during the design phase of NextGen, and tie this design to on-board capabilities to provide runtime System Health Management (SHM), ensuring the safety of people and property on the ground. This proposal takes a holistic view and integrates advances in the state of the art from three intertwined perspectives to address safe integration of unmanned systems into the national airspace: from on-board the vehicle, from the environment (NAS), and from the underlying theory enabling their formal analysis. There has been rapid development of new UAS technologies yet few of them are formally mathematically rigorous to the degree needed for FAA safety-critical system certification. This project bridges that gap, integrating new UAS and air traffic control designs with advances in formal analysis. Within the wealth of promising directions for autonomous UAS capabilities, this project fills a unique need, providing a direct synergy between on-board UAS SHM, the NAS environment in which they must operate, and the theoretical foundations common to both of these.
This research will help to build a safer NAS with increased capacity for UAS and create broadly impactful capabilities for SHM on-board UAS. Advancements will require theoretical research into more scalable model checking and debugging of safety properties. Safety properties express the sentiment that “something bad does not happen” during any system execution; they represent the vast majority of the requirements for NextGen designs and all requirements researchers can monitor on-board a UAS for system heath management during runtime. This research will tackle new frontiers in embedding health management capabilities on-board UAS. Collaborations with aerospace system designers at the National Aeronautics and Space Administration and tool designers at the Bruno Kessler Foundation will aid real-life utility and technology transfer. Broader impact will be achieved by involving undergraduate students in the design of an open-source, affordable, all-COTS and 3D-printable UAS, which will facilitate flight testing of this project’s research advances. An open-UAS design for academia will be useful both for classroom demonstrations and as a research platform. Further impact will be achieved by using this UAS and the research it enables in interactive teaching experiences for K-12, undergraduate, and graduate students and in mentoring outreach specifically targeted at girls achieving in Science, Technology, Engineering and Mathematics (STEM) subjects.
Filed under Awards, News Features
Parallella has found our research and featured us on their website with the headline Parallella Flies with NASA!
Parallella has featured our NASA Technical Memorandum::
However, the Parallella FPGA is actually featured in several of our publications, including:
Filed under Laboratory Collaborations, News Features
The Ninth Layered Assurance Workshop (LAW) brought together academic and industrial researchers to push the bleeding edge of Compositional Trustworthiness.
LAW is affiliated with the Annual Computer Security Applications Conference (ACSAC).
Layered assurance encompasses “diverse manifestations of combined assurance, including composition (of assured components), incremental certification (incremental cost for incremental change), abstraction layers (building upon assurance of lower layers), and polymorphism (common assurance of variants, such as among members of a product line).”
https://www.acsac.org/2015/workshops/law/Rozier-Keynote-LAW2015.pdf
TITLE:
Layers of Formal Verification for Full-Scale NextGen Automated Air Traffic Control
ABSTRACT:
We are at the dawn of a new age in air traffic control. The airspace is full in the sense that demand for flights exceeds our capacity to add new air traffic. The time-tested current method of air traffic control has hit its scalability limit and must be replaced with a new system that is more scalable while also proving at least as safe. Now that we have the chance to redefine air traffic control from scratch, the question arises: how do we do it safely?
We explore new frontiers in symbolic model checking to scalably answer the functional allocation question: instead of analyzing one design, or comparing a pair of designs, we now need to take into account a large number of permutations and combinations of functions that comprise a large set of possible designs. We compositionally model and comparatively analyze this set with regard to safety on multiple levels, considering the full space of possible system designs both in nominal conditions and in the presence of faults. Our analysis helps NASA narrow the possible design space, saving time and cost of later-phase evaluations, identifying both novel and known problematic design configurations. We look to the future, where a componsitional approach layering different verification techniques at multiple levels will be required to build up a safety case for the final design.
Professor Kristin Yvonne Rozier teamed up with Dr. Jeff Alstott of MIT and Singapore University of Technology to give a forward-looking presentation on “Company Network Analysis” for the World Bank Group’s “Teams Working on Corruption, Procurement, & Data Analysis: a ‘Hands-on Workshop’ on progress and future planning on using data to identify and address corruption in procurement” in Washington, D.C. on October 5, 2015. The presentation highlighted the analysis completed at the Data Science for Social Good (DSSG) program at the University of Chicago in the years 2014-2015 and a vision for increasing precision and effectiveness of the analysis using a formal methods solution.
Presentation on Company Network Analysis at the World Bank Group Workshop
Kristin Y. Rozier presenting a Formal Methods vision for the future of World Bank procurement efforts to better combat corruption.
Kristin Y. Rozier and Jeff Alstott answer questions on their proposed data pipeline.
Members of the teams from two years of Data Science for Social Good were reunited with their World Bank collaborators at the meeting. Presenters included Eric Rozier and Jeff Alstott from the 2014 DSSG fellowship and Emily Grace, Elissa Redmiles, and Kristin Y. Rozier from the 2015 fellowship, and long-time DSSG Research Fellow Matt Gee.
Data Scientists at the World Bank: {L->R]: Matt Gee, Betsy Wiramidjaja, Wolfgang Koehling, Jeff Alstott, Alexandra Habershon, Emily Grace, Elissa Redmiles, Eric Rozier, Kristin Y. Rozier, Mihaly Fazekas
Filed under Laboratory Collaborations, Research Talks
