Composition of Verification Assets for Software Product Lines of Cyber Physical Systems

The emerging Internet of Things (IoT) has facilitated an explosion of everyday items now augmented with networking and computational features. Some of these devices are developed using a Software Product Line (SPL) approach in which each device, or product, is instantiated with unique features while reusing a common core. The need to rapidly develop and deploy these systems in order to meet customer demand and reach niche markets first requires shortened development schedules. However, many of these systems perform roles requiring thorough verification, for example, securing homes. In these systems, the detection and correction of errors early in the development life cycle is essential to the success of such projects, with particular emphasis on the requirements and design phases where approximately 70% of faults are introduced. Tools such as the Architecture Analysis & Design Language (AADL) and its verification utilities aid in the development of an assured design for embedded systems. However, while AADL has excellent support for the specification of SPLs, current verification utilities for AADL do not fully support SPLs, particularly SPL models utilizing composition. We introduce an extended version of AGREE, a verification utility for AADL, with support for compositional verification of SPLs.