Identical tasks and counter variables in an integer programming-based approach to verification

摘要

A series of workshops, of which this Seventh InternationalWorkshop on Software Specification and Design (IWSSD-7) is thelatest instance, was begun in 1982. The first five of theseworkshops were held in conjunction with the InternationalConference on Software Engineering (ICSE). Specifically, the firstworkshop occurred in Kyoto following ICSE-6 (Tokyo, 1982), thesecond followed ICSE-7 (Orlando, 1984), the third followed ICSE-8(London, 1985), the fourth followed ICSE-9 (Monterey, 1987) and thefifth followed ICSE-11 (Pittsburgh, 1989). The two most recentoccurrences of the workshop have continued both the internationalcharacter and the connection to major software engineeringconferences that marked their predecessors. IWSSD-6, held in Comoin 1991, followed the Third European Software EngineeringConference (Milan, 1991). This seventh IWSSD is being held inRedondo Beach, immediately preceding the 1993 SigSoft Symposiumentitled "Foundations of Software Engineering.">IWSSD-7, like its predecessors, is intended to provide a forumfor exploring major trends and key issues in the specification anddesign of software. The format of the workshop will follow themodel that has proven so successful in the previous meetings inthis series: A fairly small number (approximately 80) ofparticipants, selected on the basis of submitted papers, will spendmost of the two day meeting discussing specific topics in one offive parallel working groups. Three plenary sessions will bring allthe workshop participants together, once for an opening address (byProfessor Tom Maibaum) and twice for presentation and discussion ofthe various working groups' deliberations.>Of course, the format is only one reason for the success ofthese workshops. The primary factor in that success is theinvestment of time, energy, insight, and enthusiasm that has beenmade by many dedicated individuals over the years. The presentmeeting, IWSSD-7, has been fortunate to have Martin Feather andAxel van Lamsweerde as its program co-chairs. Martin and Axel tookthe lead in identifying a set of workshop themes that both reflectand define the directions of current research and practice insoftware specification and design. They then selected an excellentprogram committee, orchestrated a careful and thorough reviewprocess, and assembled a very strong technical program and set ofparticipants for this meeting. We all owe them a great debt ofgratitude for their contributions to IWSSD-7. Similarly, theprogram committee members deserve our thanks for their efforts inreviewing the submitted papers, selecting the participants anddefining the working groups. A particularly important contributionhas been made by the chairs of the five working groups, who wereresponsible for the detailed planning of the activities ofthen-respective groups. Their efforts, and the active involvementof workshop participants in the various working groups' activities,are the ultimate basis for the success of 1WSSD-7. Finally, wegratefully acknowledge the cooperation of the organizingcommitteeof the 1993 SigSoft Symposium on Foundations of SoftwareEngineering, especially Hal Hart's invaluable role as localarrangements chair of both the SigSoft meeting and IWSSD-7.>On behalf of Martin, Axel and the rest of the IWSSD-7 programcommittee, I hope that you will find this workshop a source ofvaluable information regarding the current state of research andpractice in the field of software specification and design. Perhapsit will inspire you to work toward future advances in this fieldand to consider participating in the next International Workshop onSoftware Specification and Design. In the end, your reactions tothis meeting will be the truest measure of its success and yourinterest in future participation will be a significant factor inthe ongoing success of the IWSSD series.>IWSSD-7 is the seventh in a series of workshops that wereinformally set up 11 years ago with the goal of exploring majortrends and key issues in the specification and design of softwaresystems. This series hasgained interest because it has establisheda unique combination of features useful for the research community- namely, the organization focused on discussions withinparallel working groups (rather than formal paper presentations)together with group interaction through plenary sessions, itcaptured the pre- and post-workshop states through high-qualityproceedings and discussion summaries, and it assessed the concepts,models and methods discussed during the workshop through a commonset of practical examples that have flourished from one workshop tothe next. As in the past, we have tried to avoid the insularitytrap by organizing the workshop in conjunction with a majorsoftware engineering conference - such as SIGSOFTSymposium on the Foundations of Software Engineering this year- because of significant overlap in themes andapproaches.>Participation in the workshop continues to be limited to aselect number of researchers, chosen on the basis of a submittedpaper. Besides technical papers and position statements, the Callfor Papers this time solicited a third category, that of experiencepapers. There has been a continuing emphasis on formal techniquesfor capturing and analyzing specification/design products andprocesses. But, as Dana Scott pointed out, "formalization is anexperimental science" (D.S. Scott, Background to Formalization InTruth, Syntax and Modality, H. Leblanc, ed., North Holland, 1973,pp. 243-273.) We really need more insight from sizable experimentsto guide the elaboration of new formal techniques and theassessment and solidification of existing ones.>We received a total of 88 submissions. They continue to reflecta truly international spectrum of work - 22 countriesspanning 4 continents are represented. Out of these, the paperspublished here comprise those judged best by the Program Committee.The selection contains 3 experience papers, 4 position papers, and16 regular papers. There was a relatively even distribution ofsubmissions across all of the workshop's major themes:>• Requirements Engineering>• Real-time Systems>• Concurrency and Distribution>• Formal Reasoning>• Design Methods and Software Architectures>These themes obviously are not orthogonal. Some of the papersmight have been classified in other categories and some of theexperience papers may alternatively be seen as "technical"papers.>Each major theme above defines a workshop track for which twocoordinators have been nominated. We owe much to the dedicatedefforts of these track chairs. They are assigned the difficult taskof establishing the principles and rules according to which theirgroup will be working, they have to summarize the group discussionsduring the plenary sessions, and they are responsible for conveyingthe essence of the group work in the workshop summaries that willappear subsequently in a professional publication.>Besides the track chairs, we would like to express our warmestthanks to all members of the Program Committee who have beenworking hardreviewing papers and making suggestions regarding theworkshop. We are also indebted to all chairs of the previousIWSSD's for establishing the principles on which IWSSD-7 relies. Wewould finally like to thank all submittors for providing input tothese two days of exciting discussions.