Radu Siminiceanu
Work Address : 100 Exploration Way, Suite 105A, Hampton, VA 23666
Tel: (757) 325 6910
Fax: (757) 325 6988
Email: radu@nianet.org
Personal Website Address: http://research.nianet.org/~radu
Research Interests
• Formal Methods; Formal Verification
• Static Analysis
• Model Checking; Symbolic Model Checking; Decision Diagrams
• Air Traffic Management
• Avionics Software
Current Research
• "Formal Verification and Automated Testing for Diagnostic and Monitoring Systems Using Hybrid Abstraction". The central theme of this project is the use of hybrid abstraction to support both verification and testing. Hybrid abstraction is a static analysis method based on constructing sound abstractions of hybrid systems, while preserving sufficient properties for analysis. Discrete abstractions constructed by this method are finite systems that can be analyzed using the existing capabilities of symbolic model checkers. However, these systems are likely to be computationally expensive to analyze. The part of the project that NIA is involved in is improving the SAL tool with advanced model-checking techniques, such as the saturation procedure for state-space construction and the Multiway Decision Diagrams (MDD) data-structure available in the model checker SMART.
• “Integrating Human Factors and Formal Methods”: Complex, safety-critical systems proposed for NextGen involve the interaction of human operators (pilots and air traffic controllers) with automated devices. Failures in such safety-critical systems are generally not due to a single system element, but rather multiple entities that interact in unexpected ways. A common source of such problems is the interaction between human operators and other system components. For example, erroneous human behavior has contributed to over 70% of all general aviation accidents and at least two-thirds of commercial aviation accidents. Because both human factors and formal methods are concerned with the engineering of robust systems that will not fail under realistic operating conditions, we utilize human factors modeling concepts with the powerful verification techniques of formal methods to find potential problems in safety-critical systems. This approach is based on formalizing human task behavior and incorporating a popular taxonomy of typical human errors.
Publications
Journal papers:
• Jonathan Ezekiel, Gerald Lüttgen, Radu Siminiceanu, "To Parallelise or to Optimise?", PDMC special edition, Journal of Logic and Computation, Feb 2009, Oxford Press.
• Radu Siminiceanu, Gianfranco Ciardo, "Formal Verification of the NASA Runway Safety Monitor",.Software Tools for Technology Transfer (STTT), vol 9(1), p.63-76, 2007.
• Gianfranco Ciardo, Robert Marmorstein, Radu Siminiceanu, "The saturation algorithm for symbolic state space exploration", Software Tools for Technology Transfer (STTT) Vol.8 (1), p.4-25, pp.4-25, 2006.
Conference papers:
• Andy Galloway, Jan Tobias Mühlberg, Gerald Lüttgen, Radu Siminiceanu, "Model-checking the Linux Virtual File System", Verification, Model Checking, and Abstract Interpretation (VMCAI 2009), Savannah, Jan 2009.
• Bruno Dutertre, John Rushby, Ashish Tiwari, Cèsar Muñoz, Radu Siminiceanu, "Formal Verification and Automated Testing for Diagnostic and Monitoring Systems", AIAA Guidance, Navigation and Control Conference (GNC 2008), Honolulu, August 2008.
• Matthew L. Bolton, Ellen J. Bass, Radu Siminiceanu, "Using Formal Methods to predict Human Error and System Failures", 2nd Int'l Conference, Applied Human Factors and Ergonomics (AHFEI 2008), Las Vegas, July 2008.
• Radu Siminiceanu, Rick W. Butler, Cèsar A. Muñoz, "Experimental Evaluation of a Planning Language Suitable for Formal Verification", Model Checking and Artificial Intelligence (MoChArt) 2008, Patras, Greece.
• Radu Siminiceanu, Gianfranco Ciardo, "New Metrics for Static Variable Ordering in Decision Diagrams" , Tools and Algorithms for the Construction and Analysis of Systems (TACAS) 2006, LNCS 3920, pp.90-104, Vienna, Austria, March 2006.
• Gianfranco Ciardo, Radu Siminiceanu, "Structural Symbolic CTL Model Checking" , Computer Aided Verification (CAV) 2003, Boulder, Colorado, July 2003, LNCS 2725, pp.40-53.
• Gianfranco Ciardo, Radu Siminiceanu, "Using Edge-Valued Decision Diagrams for Symbolic Generation of Shortest Paths", Formal Methods in Computer Aided Design (FMCAD) 2002, LNCS 2517, pp. 256-273.
• Gianfranco Ciardo, Gerald Lüttgen, Radu Siminiceanu, "Saturation: An Efficient Iteration Strategy for Symbolic State-space Generation", TACAS 2001, LNCS 2031, pp. 328-342.