Code 5546 is the Software Engineering Section in the Center for High Assurance Computer Systems Branch of the Information Technology Division.

The section's mission is to conduct research in and to develop technology for high assurance software. The primary thrust of the research is the formulation of mathematically based methods, models, algorithms, and theories supporting both the construction as well as the analysis of software at different levels of abstraction from requirements through binary code. Researchers in the section work closely with developers and evaluators of Naval and other government systems to transfer the results of the section's research to software practice.

Model-Based Software Development and Analysis
  • Requirements Specification, Validation and Verification
  • Compositional Software Construction and Verification
  • Assertion-Based Analysis of Software Models
  • Hardware/Software Co-Design
  • Fault-Tolerant Computing
  • Real-Time Computing

Selected Publications

2009 Heitmeyer CL.  2009.  On the Role of Formal Methods in Software Certification: An Experience Report. Electronic Notes in Theoretical Computer Science . 238(4):3-9. Heitmeyer2009.pdf (189.1 KB)
2009 Jeffords R, Heitmeyer CL, Archer M, Leonard E.  2009.  A Formal Method for Developing Provably Correct Fault-Tolerant Systems Using Partial Refinement and Composition. Formal Methods, Second World Congress (FM 2009). :173-189. Jeffords etal2009.pdf (144.97 KB)
2008 [Anonymous].  2008.  Applying Infinite State Model Checking and Other Analysis Techniques to Tabular Requirements Specifications of Safety-Critical Systems. Design Automation for Embedded Systems. 12(1-2):97-137.
2008 [Anonymous].  2008.  Applying Formal Methods to a Certifiably Secure Software System. IEEE Transactions on Software Engineering. 34(1):82-98.
2007 Heitmeyer CL, Jeffords R, Bharadwaj R, Archer M.  2007.  RE Theory Meets Software Practice: Lessons from the Software Development Trenches. 15th IEEE International Requirements Engineering Conference. :265-268. Heitmeyer etal2007.pdf (521.34 KB)
2007 Heitmeyer CL.  2007.  Formal Methods for Specifying, Validating, and Verifying Requirements. Journal of Computer Science. 13(5):607-618. Heitmeyer2007.pdf (466.65 KB)
2007 Heitmeyer CL, Jeffords R.  2007.  Applying a Formal Requirements Method to Three NASA Systems: Lessons Learned. 2007 IEEE Aerospace Conference. HeitmeyerJeffords2007.pdf (616.1 KB)
2006 Archer M, Leonard E.  2006.  Establishing High Confidence in Code Implementations of Algorithms using Formal Verification of Pseudocode. Proceedings of VERIFY'06, The Third International Verification Workshop. ArcherLeonard2006.pdf (2.14 MB)
2006 Bultan T, Heitmeyer CL.  2006.  Analyzing Tabular Requirements Specifications Using Infinite State Model Checking. Fourth ACM-IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE'06). BultanHeitmeyer2006.pdf (163.42 KB)
2006 Heitmeyer CL, Archer M, Leonard E, McLean J.  2006.  Formal specification and verification of data separation in a separation kernel for an embedded system. 13th ACM Conference on Computer and Communications Security (CCS 2006). :346-355. Heitmeyer etal2006.pdf (265.8 KB)
2006 Rothamel T, Liu YA, Heitmeyer CL, Leonard E.  2006.  Generating Optimized Code from SCR Specifications. ACM SIGPLAN/SIGBED Conference on Languages, Compilers, and Tools for Embedded Systems (LCTES 2006). Rothamel etal2006.pdf (159.88 KB)
2006 Lim HP, Archer M.  2006.  Translation Templates to Support Strategy Development in PVS. STRATEGIES06, The Sixth International Workshop on Strategies in Automated Deduction. LimArcher2006.pdf (2.52 MB)
2005 Heitmeyer CL, Archer M, Bharadwaj R, Jeffords R.  2005.  Tools for constructing requirements specifications: The SCR toolset at the age of ten. International Journal of Computer Systems Science and Engineering. 20(1):19-35. Heitmeyer etal2005.pdf (774.15 KB)
2005 Leonard E, Archer M.  2005.  Extended Abstract: Organizing Automaton Specifications to Achieve Faithful Representation. Third ACM-IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE'05). LeonardArcher2005.pdf (88.94 KB)
2005 Luo J, Montrose B, Kang M.  2005.  An Approach for Semantic Query Processing with UDDI. Agents, Web Services and Ontologies Merging. Luo etal2005.pdf (240.06 KB)
2005 Mitra S, Archer M.  2005.  PVS Proof Strategies for Proving Abstraction Properties of Automata. Electronic Notes in Theoretical Computer Science. 125:45-65. MitraArcher2005.pdf (486.64 KB)
2005 [Anonymous].  2005.  Point/Counterpoint. IEEE Software. 22(1):48-51.
2005 Jeffords R, Bharadwaj R.  2005.  Extended Abstract: Formal Verification of Architectural Patterns in Support of Dependable Distributed Systems. Third ACM-IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE'05). JeffordsBharadwaj2005.pdf (59.54 KB)
2004 Heitmeyer CL.  2004.  Managing complexity in software development with formally based tools. ETAPS Workshop on Formal Foundations of Software and Component-Based Software Architectures (FESCA 2004). Heitmeyer2004.pdf (175.67 KB)
2004 Mitra S, Archer M.  2004.  Reusable PVS Proof Strategies for Proving Abstraction Properties of I/O Automata. Fourth International Workshop on Strategies in Automated Deduction (STRATEGIES 2004). MitraArcher2004.pdf (486.64 KB)
2004 Archer M.  2004.  Basing a Modeling Environment on a General Purpose Theorem Prover. 2004 Monterey Workshop on Software Engineering Tools: Compatibility and Integration. Archer2004.pdf (10.51 MB)
2004 Jeffords R, Leonard E.  2004.  Using Invariants to Optimize Formal Specifications Before Code Synthesis. 2nd ACM/IEEE Int'l Conf. on Formal Methods and Models for Co-Design (MEMOCODE 2004). JeffordsLeonard2004.pdf (127.34 KB)
2003 [Anonymous].  2003.  Developing User Strategies in PVS: A Tutorial. First International Workshop on Design and Application of Strategies/Tactics in Higher Order Logics (STRATA 2003).
2003 Archer M, Leonard E, Pradella M.  2003.  Modeling Security-Enchanced Linux Policy Specifications for Analysis. Research Summaries for DISCEX III. Archer etal2003.pdf (192.2 KB)
2003 [Anonymous].  2003.  Analyzing Security-Enhanced Linux Policy Specifications. IEEE 4th International Workshop on Policies for Distributed Systems and Networks (POLICY 2003).
2003 Bharadwaj R.  2003.  Secure Middleware for Situation-Aware Naval C2 and Combat Systems. 9th International Workshop on Future Trends of Distributed Comput ing Systems (FTDCS 2003). Bharadwaj2003.pdf (169.53 KB)
2003 Bharadwaj R.  2003.  How to Fake a Rational Design Process using the SCR Method. Software Engineering for High Assurance Systems (SEHAS 2003). Bharadwaj2003b.pdf (75.62 KB)
2003 Bharadwaj R.  2003.  A Framework for the Formal Analysis of Multi-Agent Systems. Formal Approaches to Multi-Agent Systems (FAMAS), affiliated with ETAPS 2003. Bharadwaj2003c.pdf (228.44 KB)
2003 Jeffords R, Heitmeyer CL.  2003.  A Strategy for Efficiently Verifying Requirements Specifications Using Composition and Invariants. European Software Engineering Conference/ACM SIGSOFT Symposium on the Foundations of Software Engineering (ESEC/FSE 2003). JeffordsHeitmeyer2003.pdf (211.53 KB)
2003 Kim SE, In P, Bharadwaj R.  2003.  An Extended Framework for the Validation and Verification of Situation-Aware Middleware Architectures. Proceedings Ground System Architectures Workshop (GSAW 2003). Kim etal2003.pdf (52.47 KB)
2003 Leonard E, Heitmeyer CL.  2003.  Program Synthesis from Formal Requirements Specifications using APTS. Higher-Order and Symbolic Computation. 16(1-2):63-92. LeonardHeitmeyer2003.pdf (164.15 KB)
2003 Mitra S, Archer M.  2003.  Developing Strategies for Specialized Theorem Proving about Untimed, Timed, and Hybrid I/O Automata. First International Workshop on Design and Application of Strategies/Tactics in Higher Order Logics (STRATA 2003). MitraArcher2003.pdf (159.7 KB)
2003 Bharadwaj R.  2003.  Verifiable Middleware for Secure Agent Interoperability. 2nd Goddard IEEE Workshop on Formal Approaches to Agent-Based Systems. Bharadwaj2003d.pdf (183.81 KB)
2003 [Anonymous].  2003.  Analyzing Security-Enhanced Linux Policy Specifications. NRL Memorandum Report.
2002 Archer M.  2002.  Proving Correctness of the Basic TESLA Multicast Stream Authentication Protocol with TAME. WITS '02. Archer2002.pdf (191.65 KB)
2002 Bharadwaj R.  2002.  Formal Analysis of Domain Models. International Workshop on Requirements for High Assurance Systems (RHAS'02). Bharadwaj2002.pdf (200.72 KB)
2002 Bharadwaj R.  2002.  SINS: A middleware for autonomous agents and secure code mobility. Second International Workshop on Security of Mobile Multi-Agent Systems (SEMAS-02), First International Joint Conference on Autonomous Agents and Multiagent Systems (AAMAS 2002). Bharadwaj2002b.pdf (119.17 KB)
2002 Bharadwaj R.  2002.  SOL: A Verifiable Synchronous Language for Reactive Systems. Synchronous Languages, Applications, and Programming (SLAP'02), ETAPS'2002. Bharadwaj2002c.pdf (219.78 KB)
2002 Bharadwaj R, Froscher J, Khashnobish A, Tracy J.  2002.  An Infrastructure for Secure Interoperability of Agents. Sixth World Multiconference on Systemics, Cybernetics, and Informatics. Bharadwaj etal2002.pdf (32.11 KB)
2002 [Anonymous].  2002.  Verifiable Middleware for Secure Agent Interoperability. Second Goddard IEEE Workshop on Formal Approaches to Agent-Based Systems (FAABS II).
2002 Heitmeyer CL, Marciniak JJ.  2002.  Software Cost Reduction. Encyclopedia of Software Engineering. 2 Heitmeyer2002.pdf (220.45 KB)
2002 Kirby, Jr J.  2002.  Rewriting Requirements for Design. IASTED International Conference on Software Engineering and Applications (SEA) 2002. Kirby2002.pdf (274.15 KB)
2002 [Anonymous].  2002.  Towards a Methodology and Tool for the Analysis of Security-Enhanced Linux Security Policies. NRL Memorandum Report.
2002 Archer M, Heitmeyer CL, Riccobene E.  2002.  Proving Invariants of I/O Automata with TAME. Automated Software Engineering. 9:201-232. Archer etal2002.pdf (355.28 KB)
2001 Heitmeyer CL.  2001.  Applying 'Practical' Formal Methods to the Specification and Analysis of Security Properties. Information Assurance in Computer Networks (MMM-ACNS 2001). Heitmeyer2001.pdf (137.38 KB)
2001 Jeffords R, Heitmeyer CL.  2001.  An Algorithm for Strengthening State Invariants Generated from Requirements Specifications. Fifth IEEE Int'l Symp. on Requirements Engineering (RE'01). JeffordsHeitmeyer2001.pdf (344.59 KB)
2000 Archer M.  2000.  TAME: Using PVS Strategies for Special-Purpose Theorem Proving. Annals of Mathematics and Artificial Intelligence. 29(1-4):139-181. Archer2000.pdf (462.98 KB)
2000 [Anonymous].  2000.  Using TAME to Prove Invariants of Automata Models: Two Case Studies. Third ACM Workshop on Formal Methods in Software Practice (FMSP'00). :25-36.
2000 Bharadwaj R, Heitmeyer CL.  2000.  Developing High Assurance Avionics Systems with the SCR Requirements Method. 19th Digital Avionics Systems Conference. BharadwajHeitmeyer2000.pdf (71.48 KB)
2000 Bharadwaj R, Sims S.  2000.  Salsa: Combining Constraint Solvers with BDDs for Automatic Invariant Checking. Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2000). BharadwajSims2000.pdf (265.25 KB)
2000 Heitmeyer CL, Bharadwaj R.  2000.  Applying the SCR Requirements Method to the Light Control Case Study. Journal of Universal Computer Science. HeitmeyerBharadwaj2000.pdf (363.13 KB)
2000 Riccobene E, Archer M, Heitmeyer CL.  2000.  Applying TAME to I/O Automata: A User's Perspective. NRL Memorandum Report. Riccobene etal2000.pdf (318 KB)
1999 Bharadwaj R, Heitmeyer CL.  1999.  Model Checking Complete Requirements Specifications Using Abstraction. Automated Software Engineering. 6(1):37-68. BharadwajHeitmeyer1999.pdf (171.03 KB)
1999 Gargantini A, Heitmeyer CL.  1999.  Using Model Checking to Generate Tests from Requirements Specifications. Joint 7th Eur. Software Engineering Conf. and 7th ACM SIGSOFT Intern. Symp. on Foundations of Software Eng. (ESEC/FSE99). GargantiniHeitmeyer1999.pdf (261.95 KB)
1999 [Anonymous].  1999.  SCR: A Practical Approach to Building a High Assurance COMSEC System. 15th Annual Computer Security Applications Conference (ACSAC '99).
1998 Heitmeyer CL.  1998.  On the Need for 'Practical' Formal Methods. Formal Techniques in Real-Time and Real-Time Fault-Tolerant Systems, 5th Intern. Symposium (FTRTFT'98). LICS 1486:18-26. Heitmeyer1998.pdf (138.88 KB)
1998 Heitmeyer CL, Kirby, Jr J, Labaw B, Bharadwaj R.  1998.  SCR*: A Toolset for Specifying and Analyzing Software Requirements. Computer-Aided Verification, 10th Ann. Conf. (CAV'98). Heitmeyer etal1998.pdf (154.77 KB)
1998 Heitmeyer CL, Kirby, Jr J, Labaw B, Archer M, Bharadwaj R.  1998.  Using Abstraction and Model Checking to Detect Safety Violations in Requirements Specifications. IEEE Transactions on Software Engineering. 24(11) Heitmeyer etal1998b.pdf (897.72 KB)
1998 Jeffords R, Heitmeyer CL.  1998.  Automatic Generation of State Invariants from Requirements Specifications. 6th International Symposium on the Foundations of Software Engineering (FSE-6). JeffordsHeitmeyer1998.pdf (344.8 KB)
1998 Archer M, Heitmeyer CL, Sims S.  1998.  TAME: A PVS Interface to Simplify Proofs for Automata Models. UITP. Archer etal1998.pdf (199.67 KB)
1998 Archer M, Heitmeyer CL.  1998.  Mechanical Verification of Timed Automata: A Case Study. NRL Memorandum Report. ArcherHeitmeyer1998.pdf (678.22 KB)
1997 Archer M, Heitmeyer CL.  1997.  Human-Style Theorem Proving Using PVS. TPHOLs. ArcherHeitmeyer1997.pdf (220.72 KB)
1997 Archer M, Heitmeyer CL.  1997.  Verifying Hybrid Systems Modeled as Timed Automata: A Case Study. HART. ArcherHeitmeyer1997b.pdf (178.46 KB)
1997 Bharadwaj R, Heitmeyer CL.  1997.  Verifying SCR Requirements Specifications using State Exploration. First ACM SIGPLAN Workshop on Automatic Analysis of Software. BharadwajHeitmeyer1997.pdf (248.61 KB)
1997 Bharadwaj R, Heitmeyer CL.  1997.  Applying the SCR Requirements Method to a Simple Autopilot. Fourth NASA Langley Formal Methods Workshop. BharadwajHeitmeyer1997b.pdf (289.85 KB)
1996 Archer M, Heitmeyer CL.  1996.  Mechanical Verification of Timed Automata: A Case Study. 996 Real-Time Technology and Applications Symposium. ArcherHeitmeyer1996.pdf (232.16 KB)
1996 Archer M, Heitmeyer CL.  1996.  TAME: A Specialized Specification and Verification System for Timed Automata. Work in Progress session at RTSS. ArcherHeitmeyer1996b.pdf (134.07 KB)
1996 Heitmeyer CL, Jeffords R, Labaw B.  1996.  Automated Consistency Checking of Requirements Specifications. ACM Transactions on Software Engineering and Methodology. 5(3):231-261. Heitmeyer etal1996.pdf (394.91 KB)
1995 Heitmeyer CL, Labaw B.  1995.  Consistency Checking of SCR-Style Requirements Specifications. International Symposium on Requirements Engineering. HeitmeyerLabaw1995.pdf (257.28 KB)
1995 Heitmeyer CL, Bull A, Gasarch C, Labaw B.  1995.  SCR*: A Toolset for Specifying and Analyzing Requirements. Tenth Annual Conference on Computer Assurance (COMPASS '95). :109-122. Heitmeyer etal1995.pdf (388.92 KB)
1995 McLean J, Heitmeyer CL.  1995.  High Assurance Computer Systems: A Research Agenda. America in the Age of Information, National Science and Technology Council Committee on Information and Communications Forum. McLeanHeitmeyer1995.pdf (103.99 KB)
1994 Heitmeyer CL, Lynch N.  1994.  The Generalized Railroad Crossing: A Case Study in Formal Verification of Real-Time Systems. NRL Memorandum Report. HeitmeyerLynch1994.pdf (242.1 KB)
1994 Heitmeyer CL, Lynch N.  1994.  The Generalized Railroad Crossing: A Case Study in Formal Verification of Real-Time Systems. IEEE Real-Time Systems Symposium. HeitmeyerLynch1994b.pdf (311.85 KB)
1994 Heitmeyer CL.  1994.  The Role of HCI in CASE Tools Supporting Formal Methods. Workshop on Software Engineering an human-Computer Interaction. Heitmeyer1994.pdf (16.11 KB)
1993 Clements P.C, Heitmeyer CL, Labaw B, Rose A.T.  1993.  MT: A toolset for specifying and analyzing real-time systems. IEEE Real-Time Systems Symposium. :12-22. Clements etal1993.pdf (841.51 KB)
1993 Heitmeyer CL, Labaw B, Jeffords R.  1993.  A Benchmark for Comparing Different Approaches for Specifying and Verifying Real-Time Systems. Tenth IEEE Workshop on Real-Time Operating Systems and Software. Heitmeyer etal1993.pdf (95.56 KB)