Ben Kaizi-Lutu

CSE 584 Software Engineering

Requirements and specification

M. Jackson and P. Zave. Deriving Specifications from Requirements: An Example. In Proceedings of the 17th International Conference on Software Engineering (April 1995). N.G.

Requirements and specifications are separately defined and clarified in language very typical of Michael Jackson's work. Requirements are identified with the enviroment or the world while specifications are identified with the machine. We can start from requirements and derive specifications because specifications are really restricted requirements. Specifications are therefore requirements that have been stripped of every environment phenomena that are not accessible to the machine. The example used is that of a turnstile at a zoo entrance. The example conveniently allows easy separation of machine and enviroment something that is very fundamental to the methodology outlined in the paper. It seems like everything hinges on being able to draw the line between machine and environment even to the point of having to nail down the location of control of any shared phenomena. This need for absolute separation might make the method a challenge to implement in systems where the world and the machine are tightly coupled. The need for separation is even deeper than that because we need two distinct kinds of environment description. We need to determine what are optative properties: those properties that express our wishes, and we also need to determine indicative properties: those properties that are inherent in the environment regardless of machine behavior. The method then progress by defining requirements using a notation based on predicate logic and then refining them to arrive at the specification. The fact that I am not really familiar with the notation made it doubly hard for me to understand the process of reduction. However it appears that once the notation becomes familiar then progress would be much faster. A very important insight pointed out by the authors is that if this methodology is to be applied to larger systems then it may be neccessary to break the large system into smaller tractable domains.

Leveson, M.P.E. Heimdahl, H. Hildreth and J.D. Reese. Requirements Specification for Process-Control Systems. In IEEE Transactions on Software Engineering 20,9, pp. 684--707 (September 1994).

We are introduced to a method of writing requirements and specificatons for software systems using a collision avoidance system(TCAS) as an example. It was very refreshing to see that the users chose a real world system rather than a small impractical example which tends to be what most paper authors do. Approaching the system as a blackbox provides the level of abstraction neccessary to allow the simplification of specification and the delivery of something that can be easily reviewed. The language of the specification is RSML which is a language built on top of a Requirements State Machine. It is a little disheartening that a new specification language had to be formulated in order to represent the specification. I think that the absence of a standard language of representation in this area underscores both the difficulty of the subject matter and one of the reasons why there has been reluctant adoption by industry. It appears that it is easier to formulate a formal specification of requirements for very specialized systems. These are systems in which correctness requirements can be easily isolated and defined. The TCAS system appears to be in this category. However even with the relative simplicity of a system like TCAS, I found it hard to follow the state chart logic and some of the RSML step construction. In conclusion, the paper does a good job in demonstrating how real world software requirement specification can be very early on in the design process. However to the practictioner on the street this is still a far cry from a methodology that can be easily grasped and applied to day to day design of commercial software.

E.M. Clarke and J.M. Wing. Formal Methods: State of the Art and Future Directions. In ACM Computing Surveys 28, 4, pp. 626--643 (December 1996). Here is a postscript version of the paper that appears to be almost identical

A collection of examples underlining where formal techniques have been used succesfully and why. In discussing specification, it is noted that the current trend is to integrate different specification languages each able to handle a different aspect of the system. Personally I think that there is a great need for simplification and standardisation. If indeed formal methods are to gain widespread use then a higher level of standardisation is a must. Verification is a step beyond specification. There are two popular approaches to verification: model checking and theorem proving. Model checking is state space search in the system to verify that a property holds in the system. The challenge here is to devise algorithms and data structures that are efficient in handling large search spaces. Theorem proving on the other hand is automated and relatively fast. In this technique, both the specification and the system are given as automatons and compared to determine conformance. Concerning tools and methods, we are told that no one tool or method can be reliably used to analyze every part of a complex system and that a combination of tools and methods would need to be applied. What this really means is that the learning curve is pretty steep for those who would like to adopt such methods as practictioners. And the other question that it poses is that would the realized gains be worth the upfront effort needed to adopt such methods? The authors do well to note that education is one of the areas that can be used to help further the future of formal methods. Personally this class has been the first forum in which I have been introduced to formal methods as a part of the software design process. In my discussions with other practicing engineers I have observed that only a small cross-section of them have had any training in formal methods and these tend to be the folks who were math majors in college

Formal Methods: Point-Counterpoint. In Computer 29,4, pp. 18--30 (April 1996).

This paper made for the most pleasant reading in this collection. What I found most interesting is the overall agreement that there is a chasm between academia and industry on the importance and practicality of formal methods as viable tool in software engineering. The chasm is at the foundation of the different viewpoints held by proponents in either domain. These viewpoints are as wide as academics stating that "formal methods are inevitable" while practictioners claim "formal methods are irrelevant".

Some of the authors propose using 'lightweight' formal methods. In this method the exercise begins in identifying those portions of the system that would benefit from a formal approach. Even if it may sound like a classical compromise, this method sounds very appealing and practical from the practictioner's viewpoint and may indeed be the only way that formal methods are ever implemented in the industrial field. My personal opinion is that the arguments would subside to some extent if there were a collection of tools that were easily adaptable to the various engineering needs of industry. These tools would lessen the requirement for every practioner to be fluent in formal methods. I think that the learning curve being as steep as it is in a field whose returns are not yet easily quantifiable makes it very discouraging for commercial engineers to justify the cost of such an endeavour. For the most part, the technologies that have been adopted and used widely in industry have always been accompanied by great tools. Call them compilers, linkers, interpreters, debuggers, Integrated Development Environments; all these have been tools that enable proffesionals to quickly roll out products to the market. There is still too many wheels to be invented in the formal methods field and I think the burden largely rests on academics to first of all elevate formal methods as an important part of educationa and research. Hopefully this will lead to breakthroughs in specification language and notation leading to better standardisation. The key should be "let the machine analyze the machine". As a practictioner what I am waiting for is a tool I can start and be prompted to enter my requirements in plain english and have it generate my specification in some intermediate format that can then be used for verification. Until I get this tool, I must continue to question wether formal methods are not just a way of reducing software malleability and of producing non-human readable specifications.