Stalnaker's Epistemic Logic by Laura P. Gamboa Guzman This work is a formalization of Stalnaker's epistemic logic with countably many agents and its soundness and completeness theorems, as well as the equivalence between the axiomatization of S4 available in the Epistemic Logic theory and the topological one. It builds on the Epistemic Logic theory. https://www.isa-afp.org/entries/Stalnaker_Logic.html
Category Archives: Publication Highlights
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).
Cristian Mattarei presents at FMCAD 2015: “Comparing Different Functional Allocations in Automated Air Traffic Control Design“
PhD candidate Cristian Mattarei gave a wonderful presentation of our work on “Comparing Different Functional Allocations in Automated Air Traffic Control Design” by Cristian Mattarei, Alessandro Cimatti, Marco Gario, Stefano Tonetta, and Kristin Y. Rozier today at Formal Methods in Computer-Aided Design (FMCAD) 2015 at the University of Texas at Austin. Our paper stems from a fruitful collaboration with the Embedded Systems Laboratory at the Fondazione Bruno Kessler (FBK) in Trento, Italy.
The slides are available here.
In the early phases of the design of safety-critical
systems, we need the ability to analyze the safety of different
design solutions, comparing how different functional allocations
impact the overall reliability of the system. To achieve this
goal, we can apply formal techniques ranging from model
checking to model-based fault-tree analysis. Using the results
of the verification and safety analysis, we can compare different
solutions and provide the domain experts with information on
the strengths and weaknesses of each solution.
In this paper, we consider NASA’s early designs and functional
allocation hypotheses for the next air traffic control system for
the United States. In particular, we consider how the allocation of
separation assurance capabilities and the required communication
between agents affects the safety of the overall system. Due
to the high level of details, we need to abstract the domain while
retaining all of the key properties of NASA’s designs. We present
the modeling approach and verification process that we adopted.
Finally, we discuss the results of the analysis when comparing
different configurations including both new, self-separating and
traditional, ground-separated aircraft.
Reproducibility, Correctness, and Buildability: the Three Principles for Ethical Public Dissemination of Computer Science and Engineering Research
Our paper has been published in IEEE Ethics 2014! This is the first collaboration with the Trustworthy Data Engineering Lab: Reproducibility, Correctness, and Buildability: the Three Principles for Ethical Public Dissemination of Computer Science and Engineering Research.
Dr. Kristin Y. Rozier (NASA ARC), in collaboration with Dr. Julia Badger (NASA JSC), served as Programme Committee chairs of the sixth annual NASA Formal Methods Symposium (NFM), held April 29 through May 1, 2014. Dr. Michael Hinchey (NASA GSFC) served as General Chair. NFM 2014 was held in the Gilruth Center at NASA JSC in Houston, Texas; JSC gave NFM a warm welcome, sending Steve Stich, Deputy Director of Engineering, to deliver a welcome address on the center’s behalf.
NFM is a selective, fully peer-reviewed publication venue that attracts high-quality original research. The symposium is the result of a collaboration between formal methods researchers at six NASA centers: ARC, JPL, LaRC, JSC, GSFC, and AFRC.
NFM 2014 received 107 abstract submissions, 83 of which resulted in full papers: in total 50 regular papers describing fully developed work and complete results; and 33 short papers describing tools, experience reports, or descriptions of work in progress with preliminary results. Out of these, 20 regular papers and 9 short papers were accepted, giving an overall acceptance rate of 35% (a 40% rate for regular papers and a 27% rate for short papers). All submissions went through a rigorous reviewing process, where each paper was read by at least three reviewers.
In addition to the refereed papers, the symposium featured three invited talks and a panel feature. NASA provided a special guest talk on “NASA Future Challenges in Formal Methods,” delivered by Bill McAllister, Chief, Safety and Mission Assurance, International Space Station Safety Panels, Avionics and Software Branch, NASA Johnson Space Center. Professor Lawrence C. Paulson from the University of Cambridge gave a keynote talk on “Theorem Proving and the Real Numbers: Overview and Challenges.” Professor Moshe Y. Vardi from Rice University gave a keynote talk on “Compositional Temporal Synthesis.”
The NFM 2014 panel feature, titled “Future Directions of Specifications for Formal Methods,” featured panelists Matt Dwyer of the University of Nebraska, Hadas Kress-Gazit of Cornell University, and Moshe Y. Vardi of Rice University. Specifications are required for all applications of formal methods yet extracting specifications for real-life safety critical systems often proves to be a huge bottleneck or even an insurmountable hurdle to the application of formal methods in practice. This is the state for safety-critical systems today and as these systems grow more complex, more pervasive, and more powerful in the future, there is not a clear path even for maintaining the bleak status quo. Therefore, NFM 2014 highlighted this issue in the home of an important critical system, the Mission Control Center of NASA’s most famous critical systems, and asked our panelists where we can go from here.
NFM 2014 was attended by over a hundred formal methods researchers from around the world. Springer published the NFM symposium proceedings as a volume in the Lecture Notes of Computer Science (LNCS) series: http://link.springer.com/book/10.1007/978-3-319-06200-6.
The international program committee (PC) for NFM 2014 consisted of some of the most prominent researchers in the field of formal verification. In total, the PC consisted of 44 members from NASA, academia, industry, and other government labs who were aided in completing the extensive peer reviews by 53 additional expert external reviewers. The PC included ARC team members Guillaume Brat, Ewen Denney, Kristin Y. Rozier, Neha Rungta, Johann Schumann, Oksana Tkachuk, and Arnaud Venet. Additional reviewers included ARC team members Ganesh Pai and Sarah Thompson.
Plans are already underway for NFM 2015, which will be hosted by NASA JPL.
For more information, including the accepted papers, see the official NFM website: http://www.NASAFormalMethods.org
The widespread use and increasing complexity of mission- and safety-critical systems require advanced techniques that address their specification, verification, validation, and certification requirements. The NASA Formal Methods Symposium is a forum for theoreticians and practitioners from academia, industry, and government, with the goals of identifying challenges and providing solutions to achieving assurance in mission- and safety-critical systems. Within NASA such systems include autonomous robots, separation assurance algorithms for aircraft, Next Generation Air Transportation (NextGen), and autonomous rendezvous and docking for spacecraft. Moreover, emerging paradigms such as property-based design, code generation, and safety cases are bringing with them new challenges and opportunities. The focus of the symposium was on formal techniques, their theory, current capabilities, and limitations, as well as their application to aerospace, robotics, and other safety-critical systems in all design life-cycle stages. We encouraged work on cross-cutting approaches marrying formal verification techniques with advances in safety-critical system development, such as requirements generation, analysis of aerospace operational concepts, and formal methods integrated in early design stages carrying throughout system development.
The NASA Formal Methods Symposium is an annual event that was created to highlight the state of the art in formal methods, both in theory and in practice. The series is a spinoff of the original Langley Formal Methods Workshop (LFM). LFM was held six times in 1990, 1992, 1995, 1997, 2000, and 2008 near NASA Langley in Virginia, USA. In 2009 the first NASA Formal Methods Symposium was organized by NASA Ames Research Center in Moffett Field, CA. In 2010, the Symposium was organized by NASA Langley Research Center and NASA Goddard Space Flight Center, and held at NASA Headquarters in Washington, D.C. The third NFM symposium was organized by the Laboratory for Reliable Software at the NASA Jet Propulsion Laboratory/California Institute of Technology, and held in Pasadena, CA in 2011. NFM returned to NASA Langley Research Center in 2012; the Symposium was organized by the NASA Langley Formal Methods Group in nearby Norfolk, Virginia. NASA Ames Research Center organized and hosted NFM 2013, the fifth Symposium in the series. This year’s Symposium was organized via a collaboration between NASA Goddard Space Flight Center, NASA Johnson Space Center, and NASA Ames Research Center.
The topics covered by NFM 2014 include but are not limited to: model checking; theorem proving; static analysis; model-based development; runtime monitoring; formal approaches to fault tolerance; applications of formal methods to aerospace systems; formal analysis of cyber-physical systems, including hybrid and embedded systems; formal methods in systems engineering, modeling, requirements, and specifications; requirements generation, specification debugging, formal validation of specifications; use of formal methods in safety cases; use of formal methods in human-machine interaction analysis; formal methods for parallel hardware implementations; use of formal methods in automated software engineering and testing; correct-by-design, design for verification, and property-based design techniques; techniques and algorithms for scaling formal methods, e.g., abstraction and symbolic methods, compositional techniques, parallel and distributed techniques; application of formal methods to emerging technologies.
The 2009 Grace Hopper Celebration (GHC) of Women in Computing Conference features our panel on “Women and the Flat Connected World.” The panel features Meenakshi Kaul-Basu (Sun Microsystems), Bev Crair (Quantum Corporation), Claudia Galván (Microsoft Corporation), Kristin Yvonne Rozier (NASA), Lydia Ash (Google), Radha Ratnaparkhi (IBM), and Sumitha Prashanth (Sun Microsystems). See the story: GHC09: Women in the Flat Connected World.”,/A> GHC is in Tucson, Arizona, September 29-October 3, 2009.