Date Added: Mar 2012
The authors report on the modeling and formal analysis of reliability requirements in the context of an Airport Surveillance Radar system using SysML and probabilistic model checking. The system is modeled using the QuantUM modeling tool which uses the PRISM model checker as an analysis back-end. They illustrate how a complex system architecture can be modeled, what challenges have to be addressed when performing the automated property verification, and to what extent the presented automated analysis method can support the system engineering. They expect that the use of these methods will also have a strong impact on the certification process in future.