The STSLib Project: Towards a Formal Component Model Based on STS

We present the current state of our STSLib project. This project aims at defining an environment to formally specify and execute software components. One important feature is that our components are equipped with a protocol description, namely a Symbolic Transition System. These descriptions glue together a protocol with guards and input/output notations and a data type part. These sophisticated protocols are well-suited to the design of concurrent and communicating systems but verification remains a difficult challenge. We expect to narrow the gap between the design level and the programming level by providing a runtime support for STS. We give in this paper the main objectives of the STSLib project and overview its current state. We address the formal description of a component model, a specific approach to verify these systems and a survey of the operational level to execute them. These features are illustrated on a cash point case study