Real-time disturbance control
B. Chandrasekaran, Rajiv BHATNAGER, D. D. Sharma · Communications of the ACM · 1991
bens offer a very convincing demonstration of a formal development in their article using a theorem prover as an assistant.A formal development, in this case, is the derivation of an implementation from a formal specification through a n u m b e r of formally proven steps.It is only practical, as we well know, if there is a tool to check that the formal chain is not broken and to provide some guidance.The authors consider VDM developments and the corresponding proof obligations for each development step, mainly data'verification and operation decomposition.The case study is a robot controller and the tool used is the B theorem prover.The V D M development was expressed as a set of B rules; the tool was then able to automatically generate the proof obligations (and to prove some of them automatically).• What is especially interesting in this case study is that the formalization in B of the V D M development is independent of the case study and can be reused for other problems.Another interesting by-product is the possibility of reusing parts of proven formal developments.It turned out that B alone is not sufficient and that more expertise on VDM development would allow more guidance in the development.However, the authors demonstrate that supporting formal development is now feasible, even if it is not yet as easy as it must be some day for widespread use.• Wileden, Wolf,Rosenblatt and Tarr propose a solution for an old, yet important, problem in software development and reuse: the interoperability of components developed in different languages and/or running on different machines.Their article presents a guided tour of various existing approaches for making heterogeneous software components communicate.The authors then present their own approach, which is based on the notion of abstract data types.It looks quite natural since the notion of information hiding is relevant here.Thus, the proposed method provides a way to allow interoperability at the specification level.A notation for describing abstract data types and language bindings of such types is provided.A prototype is described which allows type definition, language bindings, and provides a library of most common datatypes.It is clear that this approach will be of high interest for the next generation of development environments since many different types of objects, manipulated via different languages, must be managed in a convenient and transparent way.• The experience reported by Prieto-Dfaz discusses the implementation of a classification scheme for r e u s e u a topic of strong current interest.The method he describes is a reuse program based on a library of reusable software assets.In addition to the conclusions the author draws from this practical application (i.e., the importance of domain analysis), we believe it represents two additional lessons of importance.It represents a strong (yet incomplete) case study of the transfer of an idea from university research through refinement by an industrial research lab to application in a production environment.The experience also points up the ever-present, but easily overlooked, truth that h u m a n and organizational issues are often at least as important as technical issues in the successful application of new techniques to software engineering.• In conclusion, we hope the articles in this special issue help to continue and expand the all-important communication that takes place at conferences like ICSE.By presenting a sample of that communication within the software-engineering c o m m u n i t y to a broader audience, it is our fervent hope that professionals from other disciplines will join in the conversation.Only through broad, diverse and substantive communication can we hope to improve the software-engineering process.