Heber Herencia-Zapana

Tel: +1 (757) 325-6907; FAX +1 (757) 325-6701

Email: heber.herencia-zapana@nainet.org

Research Interests

  • Formal verification of control software for aeronautical systems,
  • Safety case for NextGen concepts,
  • Formal methods,
  • Air traffic management,
  • Airspace research
  • Modeling and simulation,
  • Automated reasoning,
  • Probabilistic reasoning, and
  • Verification and Validation.

Education

  • Ph.D. Electrical and Computer Engineering, Old Dominion University, Norfolk, Virginia, USA (2008)
  • M.S. Mathematics, Pontificia Universidad Catolica del Peru, Lima, Peru (2006)
  • Licentiate, Physics and Mathematics, Universidad Nacional de San Antonio Abad del Cusco (1998)

Current Research

Herencia-Zapana’s research in formal methods is focused on the construction of mathematical models, which bear properties that can be analyzed and verified by computational tools, such as theorem provers (PVS).

A formal specification is a mathematical description of a system (both software and hardware) that may be used to develop an implementation; it describes what the system should do. Formal specifications make it possible to demonstrate that a candidate system design is correct in respect to a specification in question, otherwise known as formal verification.

Herencia-Zapana’s research interest is to apply formal verification techniques to safety claim and control software. In regards to his research, a safety claim, for a system, is a statement that a system, which are subject to hazardous conditions, satisfies a given set of formal specifications within a certain range of likelihood. The research objective is to construct a mathematical framework in order to formalize a safety claim about a system with an arbitrary number of hazardous conditions in a mathematical formula that can be provide in a theorem prover (PVS).

The formal verification of control software is to ensure that the control software properties maintain their actual C code implementation. While control theory properties, such as stability proofs, are widely used on models, they are never carried over into the final code. Employing program verification techniques requires a researcher to be able to express these properties at the code level, but also to have theorem provers (PVS) that are able to manipulate the proof elements.

The research objective is to develop a framework that will deal with this challenge in two phases:

  • First, to introduce a way to express control theory properties, such as C code annotations; and
  • Second, to construct a PVS control theory library that is able to manipulate mathematical concepts.

This framework will achieve the translation of control properties expressed in the code to the representation of an associated proof obligation (PO) in PVS, while allowing the library to discharge these POS within PVS.

Recent Publications

  • W. S. Gray, H. Herencia-Zapana, L. A. Duffaut Espinosa, and O. R. Gonzalez, “Bilinear Systems Interconnections and Generating Series of Weighted Petri Nets,” Systems and Control Letters .
  • Anthony Narkawicz; César Muñoz; Heber Herencia-Zapana; George Hagen “Formal Verification of Safety Buffers for State-Based Conflict Detection”
    Proceedings of the Institution of Mechanical Engineers, Part G, Journal of Aerospace Engineering(under review)
  • Heber Herencia-Zapana, Romain Jobredeaux, Sam Owre, Pierre-Loic Garoche, Eric Feron, Gilberto Perez and Pablo Ascariz . “PVS Linear Algebra Libraries for Verification of Control Software Algorithms in C/ACSL”. NASA formal Methods. Lecture Notes in Computer science 2012.
  • Heber Herencia-Zapana, George Hagen and Anthony Narkawicz. “Formalizing Probabilistic Safety Claims”. NASA formal Methods. Lecture Notes in Computer science 2011. Volume 6617/2011, 162-176
  • Heber Herencia-Zapana, Jean-Baptiste Jeannin, and Cesar Munoz. “Formal verification of safety buffers for state-based conflict detection and resolu tion”. In Proceedings of 27th International Congress of the Aeronautical Sciences, ICAS 2010, Nice, France, 2010.
  • Saikou Diallo, Heber Herencia-Zapana, Jose Padilla, Andreas Tolk: “Understanding Interoperability,” Spring Simulation Multiconference, Emerging M&S Applications in Industry and Academia (EAIA’11), SCS, Boston, MA, April 2011
  • Andreas Tolk, Saikou Diallo, Heber Herencia-Zapana, Jose Padilla Model: “Theoretic Implications for Agent Languages in Support of Interoperability and Composability,” Winter Simulation Conference, Phoenix, AZ, Dec 2011
  • A. Tejada, H. Herencia-Zapana, O. R. Gonzalez, and W. S. Gray, “Mean Square Stability Analysis of Sampled-Data Supervisory Control Systems,” IEEE Conference on Control Applications, San Antonio, Texas, 2008, pp. 37-42.
  • W. S. Gray, H. Herencia-Zapana, L. A. Duffaut-Espinosa, and O. R. Gonzalez, “On Cascades of Bilinear Systems and Generating Series of Weighted Petri Nets,” Proc. 47th IEEE Conference on Decision and Control, Cancun, Mexico, 2008, pp. 4115-4120.
  • H. Herencia-Zapana, O. R. Gonzalez, and W. S. Gray, “Dynamically Colored Petri Net Representation of Nonlinear Sampled-Data Systems with Embedded Recovery Algorithms,” Proc. 46th IEEE Conference on Decision and Control, New Orleans 2007, pp. 97-102.
  • A. Tejada, H. Herencia-Zapana, O. R. Gonzalez, and W. S. Gray, “Mean Square Stability Analysis of Hybrid Jump Linear Systems using a Markov Kernel Approach,” Proc. 2007 American Control Conference, New York City, New York, 2007, pp. 3482-3487.
  • H. Herencia-Zapana, O. R. Gonzalez, andW. S. Gray, “Towards a Theory of Sampled-Data Piecewise-Deterministic Markov Processes, ” Proc. 45th IEEE Conference on Decision and Control, San Diego, California, 2006, pp. 944-949.
  • O. R. Gonzalez, H. Herencia-Zapana, and W. S. Gray, “Stochastic Stability of Nonlinear Sampled-Data Systems with a Jump Linear Controller,” Proc. 43rd IEEE Conference on Decision and Control, Nassau, Bahamas, 2004, pp. 4128-4133.
  • S. Patilkulkarni, H. Herencia-Zapana, W. S. Gray, and O. R. Gonz´alez, “On the Stability of Jump-Linear Systems Driven by Finite-State Machines with Markovian Inputs,”Proc. 2004 American Control Conference, Boston, Massachusetts, 2004, pp. 2534-2539.
  • O. R. Gonzalez, H. Herencia-Zapana, and W. S. Gray, “Stochastic Stability of Sampled Data Systems with a Jump Linear Controller,” Proc. 36th IEEE Southeastern Symposium on System Theory, Atlanta, Georgia, 2004, pp. 256-260.