A Formal Methodology for Engineering Trustworthy Software-intensive Systems

We present a methodology based on formal languages for designing, modelling, analysing, programming and deploying software-intensive, distributed, concurrent, cyber-physical systems. The generic methodology consists of (i) a specification language equipped with a formal semantics; (ii) verification techniques, possibly based on a logic describing properties of interest; (iii) a programming framework and the related runtime environment. The challenge for language designers is to devise appropriate abstractions and linguistic primitives to deal with the specificities of the systems under consideration. We briefly overview previous achievements of the instantiation of this methodology in the service-oriented domain. We then introduce recent research activities in the autonomic computing domain, with special focus on the development and enforcement of policies for access control, resource usage, and adaptation. We conclude with an outlook of possible developments of this methodology.