The Formal Methods and Tools (FM&&T) group of the Institute for Information Science and Technologies (ISTI) of the Italian National Research Council (CNR) has a longstanding experience in research on the development and application of formal methods and software tools to specify and verify complex computer systems. In recent years, researchers from FM&&T have worked together with think3, Inc. in order to apply formal modelling and verification techniques to enhance think3's Product Data Management (PDM) groupware application thinkteam. This activity is conducted in the context of the Italian research project tocai.it, which aims at the application and development of knowledge-based technologies to support the aggregation of enterprises over the Internet. think3 is one of the industrial partners in this project.
The goal of Product Lifecycle Management (PLM) is to effectively manage a company's products across their lifecycles. think3's thinkPLM is a suite of integrated PLM applications, built on the thinkteam application, to cater for the product/document management needs of design processes in the manufacturing industry. It allows enterprises to capture, organise, automate and share engineering information in an efficient way, and is used to manage data for products/documents with long or short lifecycles.
The thinkteam groupware products are in continuous evolution and are used by large manufacturing industries which commonly have several dislocated design departments, each of which needs reliable and efficient software systems in order to cooperate efficiently. The many inherent concurrency aspects that think3 needs to address when producing their software, and their awareness of the difficulties this implies when assessing the quality of their products, have led to them becoming interested in the use of model-checking techniques during the early phases of software design.
FM&&T and think3 are thus collaborating on the employment of model-checking techniques to formalise and verify several design options for thinkteam extensions. However, we are also applying model checking to verify a number of properties related to the correctness of groupware protocols in general, ie not limited to the context of thinkteam. One of the difficulties in this domain is that detailed models tend to generate very large state spaces due to the interleaving activity that comes with many asynchronously operating clients. Therefore, our approach is to generate small, abstract models that are intended to address very specific usability-related groupware issues. This collaboration shows that model checking can be of great help in an exploratory design phase, both for comparing different design options and for refining and improving the description of the proposed extensions.
This way of using model checking is in support of a prototyping-like modelling technique. The focus is on obtaining, relatively quickly, an informed but perhaps somewhat approximate idea of the consequences, both qualitative and quantitative, of adding specific features to an existing groupware system. This differs from the traditional use of model checking as a technique to develop rather complete specifications, with the aim of reaching a maximal level of confidence in the correctness of a complicated concurrent algorithm.
An important result of the joint research concerns the uptake of model-checking techniques by industry. think3 had no previous experience with such analysis techniques. This experience with model checking specifications of a thinkteam extension has been a true eye opener for them, leading them to fully recognize the extent of the many intricate and inherent concurrency aspects of groupware systems like thinkteam.
The relatively simple, lightweight and abstract high-level models that we have developed during the collaboration have turned out to be of great help to focus on the key issues of the development of the interface aspects of thinkteam, before turning to the more detailed design and implementation issues. think3 has now expressed their intention to become more acquainted with model checking and - ultimately - to acquire the skills to perform automated verification of the (groupware) protocols underlying their software systems themselves.
This shows that our approach, which starts with small models that require little time to fully understand but that nevertheless provides results that would be unfeasible to produce manually, and can be used to generate performance diagrams directly related to issues of interest, can be successfully transferred to industry.
Links:
thinkteam and thinkPLM are registered trademarks of think3, Inc.
http://www.think3.com/
Please contact:
Maurice ter Beek or Mieke Massink
ISTI-CNR, Italy
E-mail: m.terbeek
isti.cnr.it, m.massinkisti.cnr.it
