<$BlogRSDUrl$>

Sunday, January 16, 2005

The difficulty of developing process algebras 

LUCA ACETO
Unfortunately, many realistic systems and their models exhibit behaviours that lead to state spaces too large and too complex to deal with using any of the methods above. And although we often wanted to believe differently, most of the real world examples to which we want to apply our techniques, are way out of reach.

A typical example is a new railway safety control philosophy developed in the Netherlands [4] allowing a more efficient and reliable railway transport. One of the reasons that it will not be taken into service is that nobody can convincingly certify its correct operation. Until this is possible, it seems that the Dutch railway companies will stick to the proven, simple control systems to which they are accustomed, denying customers the benefits of the new technology. In those cases where automatic methods are insufficiently helpful, manual manipulation can save the day. Typically, protocols and algorithms deal with unspecified or unbounded data, are about an unbounded number of communicating partners and are often quite complex. In order to prove the correctness of such systems human ingenuity and intuition are indispensable. The ability to include the human intellect into the verification effort will be a distinguishing success factor for many decades to come.

Topics: Workflow | Complexity


Comments: Post a Comment

This page is powered by Blogger. Isn't yours?