Aslantest: A Symbolic Execution Toolfor Testing Asian Formal Specifications *Jef?ey DouglasRichard A. KemntererReliable Software GroupDepartment of Computer ScienceUniversity of CaliforniaSanta Barbara, CA 93106AbstractThispaper introduces Aslantest, a symbolic execution tool forthe formal specification language Asian. Asian isa state-basedspecification language built on first-order predicate calculuswith equality. Mantest animates Asian specifications andenables users to interactively run specijic test cases or symboli-cally execute the specification. Testing the formal specificationsearly in the soj%vare life cycle allows one to assure a reliablesystem that also provides the desired functionality.1. IntroductionAs the size and complexity of software systems haveincreased, it has become increasingly more difficult for softwaredesigners to produce a quality product that meets the customer’srequirements in a timely manner. The problem is often a symp-tom of the informal nature of the design process. Requirementsinformally agreed upon at the beginning of the process are oftenmisunderstood or misinterpreted leadiig to &ficiencies in thefinal software product. In addition, these deficiencies are oftennot diswvered until very late in the design process, causingcostly delays in delivery.As a resul~ researchers have begun to restructure the designprocess, introducing approaches and tools, such as formalspecification and verification, which enable a designer torigorously demons~ate that an implementation is consistent withits requirements. Demonstrating that code is consistent with itscritical requirements is a difficult process. However, the processcan be made tractable by verifying the design at every step.As shown in [Kern 85] there is a problem with the approachoutlined abov~ although the specification may satisfy its criticalrequirements there may be no implementation that is consistentwith the specification and that at the same time provides thedesired functionality. To make things worse, this is usually notdiscovered until the &sign has gone through several levels ofrefinement, wifi each level being formally verified and the* This research was partially supported by the NationalComputer Security Center under grant MDA904-92-C-5149Permission to co y without fee all or part of this material isEgranted provided t at the copies are not made or distributed fordirect commercial advanta$e, the ACM copyright notice and thetitle of the publication and Its date appear, and notice is giventhat copying is by permission of the Association of ComputingMachinery. To copy otherwise, or to republish, requires a feeand/or specific permission.ISSTA 94- 8/94 Seattle Washington USA@ 1994 ACM O-89791-683-ti9410008..$3.5Oimplementation is in progress or completed. In addition, thecost of formally verifying software is high in both dollars andtime. When a &sign needs to be redone due to the discovery ofan error late in the development life cycle, the cost skyrockets.In order to reduce the cost of developing reliable systems thatalso provide the desired functionality, it is necessary to providea means to test the formal specifications early in the softwarelife cycle. The Aslsntest tool presented in this paper is a sym-bolic executor for testing Asian formal specifications to assurethat all of the functional requirements are satisfied. This pro-vides the user with a rapid prototype system early in thesoftware life cycle, and it allows the user to exercise the proto-type to see if it meets all of the anticipated needs. In addition tohelping the user tind errors in the design of the system beingdeveloped, the prototype also allows the user to find other usefulapplications for the completed system before it is delivered.A number of systems have been developed for executingstate-based formal specifications. Some of these translate thespecification into a high order language implementatio~ andothers execute the specification dinxtly. The EZ system[VN 91] is an example of the translation approach that can beused to test a subset of the Z language. It compiles Zspecifications into C-Prolog prototypes, and the user can runvarious test cases on the prototype. With this system the userprovides a start state and a result state, and the Prolog prototypeattempts to use the operations defined in the specification todetermine if the result state is accessible from the detined stsrtstate.A system that is similar to Aslantest is tie EPROS system,which is part of the VDM &velopmemt environment [HI 88].This system, compiles VDM META-IV formal specificationsinto an executable language called EPROL, which is an exten-sion of META-IV. The system provides an interactive inter-preter environment for EPROL where the user can initializevalues, execute operations, and check results. The user canexamine lwth the visible results of a sequence of operations, aswell as the internal vahtes of state variables. Like Aslantes~ theEPROS system actually animates the specification rather thanimplementing a proto~.Another system that takes a more graphical approach is theExSpect system [VSV 91], which animates Z speciticatiortsusing Petri nets. Wkb this approach tokens move about the netindicating the collection of states the system is currently in.Because tokens provide a graphical representation of how thesystem is performing, this type of system is useful for animatingspecifications of concurrent systems.15The remainder of this paper consists of four sections. Sectiontwo provides more insight into the role of formal specificationand verhication. It also reviews classifications for relating thevalidity of a functional requirement with respect to a formalspecification that were originally presented in [Kern 85]. Sec-tion three gives a brief overview of the Asian specificationlanguage. Section four describes the features and use of theAslantest symbolic execution tool and presents an example ses-sion. Finally, in the last section some concluding remarks andfuture considerations are presented.2. Formal Specification and VerificationFormal specification and verification enables a designer toshow that an implementation is consistent with its requirements.The process begins by developing a formal model of the criticalrequirements of the system, which are informally agreed uponby the customer and the developer. After these have been stated,a high level specification of the system is developed, which pre-cisely describes the behavior of the