Academic
Publications
Experience applying the SPIN model checker to an industrial telecommunications system

Experience applying the SPIN model checker to an industrial telecommunications system,10.1145/1368088.1368187,Barry Long,Juergen Dingel,T. C. Nicholas

Experience applying the SPIN model checker to an industrial telecommunications system   (Citations: 2)
BibTex | RIS | RefWorks Download
Model checking has for years been advertised as a way of ensuring the correctness of complex software systems. How- ever, there exist surprisingly few critical studies of the appli- cation of model checking to industrial-scale software systems by people other than the model checker's own authors. In this paper we report our experience in applying the Spin model checker to the validation of the failover protocols of a commercial telecommunications system. While we conclude that model checking is not yet ready for such applications, we nd that current research in the model checking commu- nity is working to address the diculties we encountered.
Cumulative Annual
View Publication
The following links allow you to view full publications. These links are maintained by other sources not affiliated with Microsoft Academic Search.
    • ...Failover is the process of returning a system to an operational state once partial failure occurred [4]...
    • ...WebArrow conferencing tool supports partial failover through off-theshelf technology [4]...

    Hongzhi Songet al. A general collaborative editing platform based on file locking mechani...

    • ...Although researchers have investigated many issues within these areas (e.g., visualizations for change awareness [21], smoothing network interruptions in streaming media [14], and data consistency algorithms [13,15,20]), there is little work on underlying design principles that will allow synchronous groupware to deal comprehensively and appropriately with periods of asynchrony...
    • ...The process of returning a system to an operational state following partial failure is termed failover [14]...
    • ...Some systems, such as the WebArrow conferencing tool, support partial failover through off-the-shelf technology such as load balancers and redundant database clusters, combined with custom algorithms for attempting to recover from failures in clients or servers [14]...

    Carl Gutwinet al. Gone but not forgotten: designing for disconnection in synchronous gro...

Sort by: