CHIC resources

• Professor Henzinger's Interfaces Papers
• chic1.2.tar.gz 5.1Mb download.
  Dirk Beyer, Arindam Chakrabarti, Krishnendu Chatterjee, Luca de Alfaro, Tom Henzinger, Marcin Jurdzinski, Freddy Mang, Cindy Song. "CHIC: Checking Interface Compatibility". Software. UC Berkeley, December, 2007.

CHIC is a modular verifier for behavioral compatibility checking of software and hardware components. The goal of CHIC is to be able to check that the interfaces for software or hardware components provide guarantees that satisfy the assumptions they make about each other. CHIC supports a variety of interface property specification formalisms: synchronous assume/guarantee interfaces, resource interfaces, web service interfaces, etc.

We propose an automata-theoretic type system for behavioral specification of open systems [1-5]. The benefit we achieve from being able to work with open systems is that we can analyze large systems incrementally without needing extensive summary information to close the system at each stage.

We have developed a formalism to behaviorally represent open web service components, a specification language to denote properties of interest in the inter-operations of such components, and algorithms to check the same [4,5]. We validate the applicability of our formalism for the specification and verification of the method-invocation behavior of web-service applications constructed from asynchronously interacting multi-threaded distributed components by modeling applications using the Amazon.com e-commerce services (ECS) framework [5].

Our algorithms for checking the behavioral compatibility of component interfaces are available in the tool Chic, which can be used as a plug-in for the Java IDE JBuilder and the heterogenous modeling and design environment Ptolemy II.

[1] L. de Alfaro and T. A. Henzinger, "Interface Automata," Proc. Symp. Foundations of Software Engineering, Vienna, Austria, September 2001.

[2] L. de Alfaro and T. A. Henzinger, "Interface Theories for Component-based Design," Proc. Int. Workshop on Embedded Software, Tahoe City, CA, October 2001.

[3] A. Chakrabarti, L. de Alfaro, T. A. Henzinger, and M. Stoelinga, "Resource Interfaces," Proc. Int. Conf. Embedded Software, Philadelphia, PA, October 2003.

[4] D. Beyer, A. Chakrabarti, and T. A. Henzinger, "Web Service Interfaces," Proc. Int. World Wide Web Conf., Chiba, Japan, May 2005.

[5] D. Beyer, A. Chakrabarti, T. A. Henzinger, and S. A. Seshia, "An Application of Web-Service Interfaces," Proc. International Conference on Web Services, Salt Lake City, UT, July 2007.

See Professor Henzinger's Interfaces Papers for more recent papers.

Chic has a BSD License

 Copyright (c) 2002-2005 The Regents of the University of California. 
 All rights reserved. 

 Permission is hereby granted, without written agreement and without 
 license or royalty fees, to use, copy, modify, and distribute this 
 software and its documentation for any purpose, provided that the 
 above copyright notice and the following two paragraphs appear in 
 all copies of this software. 

 IN NO EVENT SHALL THE UNIVERSITY OF CALIFORNIA BE LIABLE TO ANY PARTY 
 FOR DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES 
 ARISING OUT OF THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN 
 IF THE UNIVERSITY OF CALIFORNIA HAS BEEN ADVISED OF THE POSSIBILITY 
 OF SUCH DAMAGE. 

 THE UNIVERSITY OF CALIFORNIA SPECIFICALLY DISCLAIMS ANY WARRANTIES, 
 INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY 
 AND FITNESS FOR A PARTICULAR PURPOSE. THE SOFTWARE PROVIDED HEREUNDER IS 
 ON AN "AS IS" BASIS, AND THE UNIVERSITY OF CALIFORNIA HAS NO OBLIGATION 
 TO PROVIDE MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.