Dependable Global Computing
H. Bohnenkamp, T. Han, J.-P. Katoen, R. De Nicola (U. Florence, I), D. Latella and M. Massink (CNR-ISTI, I)
(funded by the DAAD and CNR-ISTI) Due to their enormous size—networks typically consist of thousands or even millions of nodes—and their strong reliance on mobility and interaction, performance and dependability issues are of utmost importance for “network-aware computing”. Spontaneous computer crashes may easily lead to failure of remote execution or process movement, while spurious network hick ups may cause loss of code fragments or unpredictable delays. The enormous magnitude of computing devices involved in global computing yields failure rates that no longer can be ignored. The presence of such random phenomena implies that correctness of global computing software and their privacy guarantees are no longer rigid notions like: “either it is safe or it is not” but have a less absolute nature, e.g.: “in 99.7% of the cases, privacy can be ensured”. The intrinsic complexity of global computers, though, complicates the assessment of these issues severely. Systematic methods, techniques and tools—all based on solid mathematical foundations i.e., formal methods, are therefore needed to establish performance and dependability requirements and guarantees.
This project attempts to make a considerable step into this direction by extending a successful programming and specification formalism for global computing, Klaim, with random delays, and by developing a novel stochastic spatial temporal logic as property specification language for performance and dependability guarantees.
H. Bohnenkamp, T. Han, J.-P. Katoen, R. De Nicola (U. Florence, I), D. Latella and M. Massink (CNR-ISTI, I)
(funded by the DAAD and CNR-ISTI) Due to their enormous size—networks typically consist of thousands or even millions of nodes—and their strong reliance on mobility and interaction, performance and dependability issues are of utmost importance for “network-aware computing”. Spontaneous computer crashes may easily lead to failure of remote execution or process movement, while spurious network hick ups may cause loss of code fragments or unpredictable delays. The enormous magnitude of computing devices involved in global computing yields failure rates that no longer can be ignored. The presence of such random phenomena implies that correctness of global computing software and their privacy guarantees are no longer rigid notions like: “either it is safe or it is not” but have a less absolute nature, e.g.: “in 99.7% of the cases, privacy can be ensured”. The intrinsic complexity of global computers, though, complicates the assessment of these issues severely. Systematic methods, techniques and tools—all based on solid mathematical foundations i.e., formal methods, are therefore needed to establish performance and dependability requirements and guarantees.
This project attempts to make a considerable step into this direction by extending a successful programming and specification formalism for global computing, Klaim, with random delays, and by developing a novel stochastic spatial temporal logic as property specification language for performance and dependability guarantees.