In this paper, we present a framework aimed at simulating control logics specified in the higher-order logic of the Prototype Verification System. The framework offers a library of predefined modules, a method for the composition of more complex modules, and an event-driven simulation engine. A developer simulates the specified system by providing its input waveforms as functions from time to logic levels. Once the simulation experiments give sufficient confidence in the correctness of the specification, the model can serve as a basis for the formal verification of desired properties of interest. A simple case study from a nuclear power plant application is shown. This paper is a contribution to research aimed at improving the development process of safety-critical systems by integrating simulation and formal specification methods.

Wireless networks are starting to be populated by interconnected devices that reveal remarkable hardware and software differences. This fact raises a number of questions on the applicability of available results on dependability-related aspects of communication protocols, since they were obtained for wireless networks with homogeneous nodes. In this work, we study the impact of heterogeneous communication and computation capabilities of nodes on dependability aspects of diffusion protocols for wireless networks. We build a detailed stochastic model of the logic layers of the communication stack with the SAN formalism. The model takes into account relevant real-world aspects of wireless communication, such as transitional regions and capture effect, and heterogeneous node capabilities. Dependability-related metrics are evaluated with analytical solutions techniques for small networks, while simulation is employed in the case of large networks.

Dynamic, evolving systems pose new challenges from the point of view of Quality of Service (QoS) analysis, calling for techniques able to combine traditional offline methods with new ones applied at run-time. Tracking the evolution and updating the assessment consistently with such system evolution require not only advanced analysis methods, but also appropriate metrics well representative of QoS properties in the addressed context. The ongoing European project Connect addresses systems evolution, and aims at bridging technological gaps arising from heterogeneity of networked systems, by synthesising on-the-fly interoperability connectors. Moving from such ambitious goal, in this paper we present a metrics framework, whereby classical dependability/QoS metrics can be refined and combined to characterise Connect applications and to support their monitoring and analysis.