A framework for formal component-based software architecting

The assessment of quality attributes of software-intensive systems is a challenging issue. This paper describes a method aimed at quantitative evaluation of certain quality attributes that are important design parameters for embedded systems; timeliness, performance and memory consumption. The following principles are important starting points for building a formal model for evaluating quality attributes: (1) Dependability constraints are specified in an end-to-end fashion; (2) Components are attributed with resource demands; (3) Specification of component interaction is separated from specification of component behavior. Furthermore, the method is aimed to be applicable in practice. Therefore we investigate combining of widely used software modeling notations with existing formal methods. In particular, the proposed approach combines Message Sequence Charts and Timed Automata. We illustrate the approach with an example.