As software systems become more and more pervasive, developing reliable and dependable systems becomes more and more critical. Software designs, which model high-level, declarative properties of intended systems, hold a key to increasing reliability and dependability. Declarative modeling is not yet a common practice, because writing declarative models correctly is still challenging and a barrier to challenging problem. To remove this impediment to the practical application of declarative (relational) modeling, the project brings software testing concepts, methods, and tool chains to formal specifications based on the Alloy relational modeling system and its underlying satisfiability solving back-ends. Such approaches include unit testing, test generation, the definition and use of coverage metrics to underpin notions of test suite adequacy, and selective regression testing in the face of small changes to specifications.
Three primary research thrusts are proposed: to build the foundations of a test-driven approach for declarative models; to define testing techniques to validate the correctness of models that users write; and to introduce sketching techniques that allow users to write incomplete models, which are completed using automated synthesis. The implementation of robust tools and a rigorous experimental evaluation based on controlled experiments and case-studies cross-cuts the research thrusts. The ability to develop correct designs, as envisioned by this project, can lead to a major increase in software reliability and dependability, which can bring substantial economic benefits and significantly improve quality of life.
