Despite years of successful research into using formal methods for the development of critical concurrent systems, there are still too many failures of critical systems in practice. Part of the reason is that use formal methods is often seen to be to costly. The Unified Modeling Language offers an unprecedented opportunity for high-quality critical systems development that is feasible in an industrial context, since many developers are trained in UML and are using it already. Our aim is to aid the difficult task of developing dependable systems in an approach based on a formal fragment of the Unified Modeling Language called UMLlight. We extend the notation to capture dependability requirements and related physical properties. This way we encapsulate knowledge on prudent dependability engineering and make it available to developers which may not be specialized in dependability. One can also go further by checking whether the constraints associated with the stereotypes are fulfilled in a given specification, by performing a formal analysis.     «

Despite years of successful research into using formal methods for the development of critical concurrent systems, there are still too many failures of critical systems in practice. Part of the reason is that use formal methods is often seen to be to costly. The Unified Modeling Language offers an unprecedented opportunity for high-quality critical systems development that is feasible in an industrial context, since many developers are trained in UML and are using it already. Our aim is to aid t...     »