A component-based approach to building formal analysis tools

• Main Authors: Kurt Stirewalt, R. E., Dillon, Laura K.
• Format: Conference Proceeding
• Language: English
• Subjects: Social and professional topics > Professional topics > Management of computing and information systems > Software management; Software and its engineering > Software creation and management; Software and its engineering > Software creation and management > Designing software; Software and its engineering > Software creation and management > Designing software > Software implementation planning > Software design techniques; Software and its engineering > Software creation and management > Software development process management > Software development methods; Software and its engineering > Software creation and management > Software verification and validation > Formal software verification; Software and its engineering > Software notations and tools > Context specific languages > Domain specific languages; Software and its engineering > Software notations and tools > Software libraries and repositories; Software and its engineering > Software organization and properties > Software functional properties > Formal methods; Software and its engineering > Software organization and properties > Software system structures > Software architectures
• DOI: 10.5555/381473.381491

Automatic-verification capability tends to be packaged into stand-alone tools, as opposed to components that are easily integrated into a larger software-development environment. Such packaging complicates integration because it involves translating internal representations into a form compatible with the stand-alone tool. By contrast, lightweight-analysis components package analysis capability in a form that does not involve such a translation. Borrowing ideas from GenVoca and object-oriented design patterns, we developed a domain model and an automatic-generation framework for lightweight-analysis components. The generated components operate directly over the internal form of a specification without requiring a change in representation. Moreover, the domain model identifies several "useful subsets" that can be used to customize analysis capability to a particular application. We validated this domain model by generating lightweight analyzers for temporal logic and the behavioral subset of Lotos.