With the goal to create autonomous systems that can accomplish complex tasks in dynamic environments, high-level software architectures are created using formal methods to describe the system with a set of elementary actions, named skills, necessary to accomplish their mission.

However, these formalisms often lack a proper framework for designing autonomous missions as a composition of the specified skills, often relying on non-formal or semi-formal tools, such as behavior trees or UML/SysML-based tools, as well as being limited to specific elementary skill implementations. This makes the system less reliable and more prone to failures when placed in a dynamic, unknown environment. To fill this gap, we propose a formal framework to specify formal models for elementary skills and make them composable, called Skill Petri nets, and a set of composition patterns and their Petri net models. A tool will allow users to define these compositions using an extension of the Robot-Language DSL, from which the formal models and a controller code are generated. An industrial inspection mission use-case allowed to test the proposed framework.