Computing Reviews
Today's Issue Hot Topics Search Browse Recommended My Account Log In
Review Help
Search
Nondeterministic modal interfaces
Bujtor F., Fendrich S., Lüttgen G., Vogler W. Theoretical Computer Science642 (C):24-53,2016.Type:Article
Date Reviewed: Nov 17 2016

Concurrent systems consist of multiple components; the design of such a system must: allow its specification to be composed from the component requirements; allow its implementation to be composed from the component capabilities; and support a process of step-wise refinement that demands more desired behaviors and prohibits more undesired ones. Such scenarios can be modeled by semantic frameworks that combine interface automata (IA), which describe the behavior of component-based systems, with modal transition systems (MTS), which describe with must-transitions and may-transitions which behavior every refinement of the system must respectively realize. However, this combination is problematic because unspecified inputs are forbidden in MTS while they lead to arbitrary behavior in IA.

This paper introduces the formalism of modal interface automata (MIA) that reconciles these views by introducing input-triggered may-transitions to a special state that can be refined in any way. The resulting theory of nondeterministic modal interfaces is elaborated in great detail by showing that it leads to a well-behaved parallel composition operator and to a quotient operator that constructs a component whose parallel composition with a given component refines a given specification, whose conjunction of specifications reflects multiple system perspectives, and whose refinement is compositional.

While the paper is mostly technical in nature, a final example demonstrates how MIA can be applied in practice. Furthermore, the authors have exploited MIA to enrich the programming language Go with behavioral types such that type checking implements refinement checking; the theory will also be implemented in formal methods tools.

Reviewer:  Wolfgang Schreiner Review #: CR144930 (1702-0142)
Bookmark and Share
  Featured Reviewer  
 
Modal Logic (F.4.1 ... )
 
 
Alternation And Nondeterminism (F.1.2 ... )
 
 
Formal Methods (D.2.4 ... )
 
 
Concurrent Programming (D.1.3 )
 
 
Requirements/ Specifications (D.2.1 )
 
Would you recommend this review?
yes
no
Other reviews under "Modal Logic": Date
A class of decidable information logics
Demri S. Theoretical Computer Science 195(1): 33-60, 1998. Type: Article
Jul 1 1998
First-order modal logic
Fitting M., Mendelsohn R., Kluwer Academic Publishers, Norwell, MA, 1999. Type: Book (9780792353348)
Mar 1 2000
Modal logic
Blackburn P. (ed), de Rijke M. (ed), Venema Y. (ed), Cambridge University Press, New York, NY, 2001.  554, Type: Book (9780521802000), Reviews: (1 of 2)
May 31 2002
more...

E-Mail This Printer-Friendly
Send Your Comments
Contact Us
Reproduction in whole or in part without permission is prohibited.   Copyright 1999-2024 ThinkLoud®
Terms of Use
| Privacy Policy