From UML activity diagrams to specification requirements

Formal verification of system-of-systems uses computer-based techniques to assure that the behavior of a subject system of systems complies with its formal correctness specifications. Such formal specifications are often created on the basis of natural-language (NL) requirement specifications. While NL documents such as marketing requirement documents and concept-of-operation (CONOPS) documents contain NL requirements, they are almost never complete, i.e., they omit necessary NL requirements. To that end, UML analysis is an increasingly popular technique for requirement elicitation. This paper describes the process of identifying NL requirements of interest from UML analysis diagrams such as activity diagrams and message sequence diagrams.