Open-world software systems are built by composing heterogeneous, third-party components, whose behavior and interactions cannot be fully controlled or predicted; moreover, the environment they interact with is characterized by frequent, unexpected, and welcome changes. An example of open-world software is represented by service-based applications, often realized by composing multiple services into a business process. Open-world software exhibits new features that demand for rethinking and extending the traditional methodologies and the accompanying methods and techniques.

In this talk I will first illustrate SOLOIST, a specification language based on a new class of specification patterns, tailored for specifying both functional and quality-of-service properties of the interactions of service compositions. I will then present an approach for verifying SOLOIST properties over service execution traces using bounded satisfiability checking techniques. The talk will also touch upon the issues of making verification incremental and shifting it to run time.