Nowadays the distributed software-intensive systems are widespread in many areas including mission-critical domains such as train, medical, automotive and aviation. Engineering of dependable software to be used in this kind of domains is the difficult task. Such advanced methods and techniques as Formal Model Verification have to be applied to provide required software quality as it is requested by field standards. 

This report contains information about related experience of Dependability Engineering group at Siemens CT Software Engineering. Formal Model Verification approach based on SPIN tool developed in Bell Labs group is shown. This approach was applied for verification of activity arbitrage algorithm between hot-reserved processing units, driver for UNIX-compatible operation system and component interaction in safety-related control system. 

The report discusses focus for analysis which could be set on different software artifacts: requirements, design specification, source code, etc. Different fault types identified in carried-out projects are shown and links with used software artifacts are given. Examples of fault types are deadlocks, livelocks, race conditions, safety violations. Benefits for software dependability depending on findings identified are discussed. 

Hints are provided and Challenges are identified for further research in this area.