Critical Systems Development with UML
Jan Jürjens, Eduardo B. Fernández, Bernhard Rumpe⋆ · 2004
In 1978, a group of researchers led by Dave Parnas developed a tabular nota- tion for specifying software requirements called SCR (Software Cost Reduction) and used the notation to specify the requirements of a mission-critical program, the Operational Flight Program for the A-7 aircraft. Since then, the require- ments of many critical programs, including control software for nuclear power plants and other flight programs, have been specified in SCR. To support for- mal representation and analysis of software requirements, NRL has developed a state machine model to define the SCR semantics and built a suite of tools based on this semantics for checking requirements specifications for properties of interest. Such tools are especially valuable for specifying and analyzing the requirements of software systems where compelling evidence is required that the system satisfies critical properties, such as safety and security properties. This talk describes the many different roles that formally based software tools can play in debugging, verifying, and validating the requirements of critical software systems. The author’s recent experience and lessons learned in specifying the requirements of a security-critical cryptographic system and two software com- ponents of NASA’s International Space System are also described. ————————————————————— Connie Heitmeyer, the chief designer of the SCR toolset, heads the Software Engineering Section of the Naval Research Laboratory’s Center for High Assur- ance Computer Systems. Recently, she served as co-program chair for MEM- OCODE 2004, the 2nd International Conference on Formal Methods in Hard- ware/Software Co-Design. She is currently serving as co-chair of the Experience Reports Track at ICSE 2005. She is a member of the editorial boards of the ACM Transactions on Software Engineering and Methodology, the Require- ments Engineering Journal, and the Journal on Software and System Modeling. Her research interests are in formal specification and formal analysis of software and system requirements and of high assurance software systems. She is also very interested in transferring formal methods technology and tools to software practitioners.