Proceedings Sixth Workshop on Formal Languages and Analysis of Contract-Oriented Software

TL;DR

This paper discusses the importance of formal languages and analysis tools for contract-oriented software in service architectures, emphasizing the need for formal reasoning and conformance testing.

Contribution

It presents FLACOS, a platform that integrates formalization, abstraction, and analysis techniques for contracts in software applications.

Findings

Development of formal models for contracts

Tools for analyzing contract conformance

Enhanced reasoning about contract compliance

Abstract

The ability to negotiate contracts for a wide range of aspects and to provide services conforming to them is a most pressing need in service-oriented architectures. High-level models of contracts are making their way into the area, but application developers are still left to their own devices when it comes to writing code that will comply with a contract concluded before service provision. At the programming language level, contracts appear as separate concerns that crosscut through application logic. Therefore there is a need for contract analysis tools that extract abstracted models from applications so they become amenable to formal reasoning using formal language techniques. Since its inception, the aim of of FLACOS has been that of bringing together researchers and practitioners working on language- or application-based solutions to these problems through the formalization of contracts, the design of appropriate abstraction mechanisms, and tools and techniques for analysis of contracts, and analysis, testing and monitoring of conformance to contracts by applications.