Software Specification

Software is a novel type of man-made product and its “engineering” is a relatively young discipline. Making software starts from requirements analysis, i.e., eliciting and specifying the goals of the stakeholders and learning about the domain in which and about which the software is going to be developed. The requirements have to be put down in terms of models or specifications. These specifications provide a firm basis for both stakeholders and software developers. They will be massaged and transformed into an architectural description of the system and further into the detailed design and finally into the implementation. In other words, all artifacts throughout the process of software development evolve from the abstract model resulting from requirements analysis and are, themselves, models at different levels of abstraction. Software specification is about such models of software: how to write them, what they mean and when to use them. It is also about methods for analyzing models: comparison of models of the same kind, checking consistency among models of different kinds and reasoning about properties of models.

Before we go into more details about our choice for models and their corresponding techniques, we would like to underscore the relevance of this notion, i.e., model, in software engineering. In all mature engineering disciplines, before building a complex structure models of such structure are made. Many calculations and experiments are made on the produced models and only when the model is proven to meet the requirements, they are going to be turned into the real constructions. Software is by no means less complex than many other products made in such branches of engineering. From early stages of requirement analysis, we need rigorous models to capture our understanding of the requirements and
put them in an unambiguous and analyzable form. After having such a rigorous model, all other steps in the development process should ideally be sound model transformations. Each of these transformations, takes a number of models at a certain abstraction level and makes a new model which is more detailed and is closer to the actual implementation, yet it preserves the correctness properties proven for the earlier models. In this sense, the final implementation is nothing but a more detailed model, which is not created from scratch but systematically developed from earlier models.
Models are not only essential for software development but also for its maintenance. Without sufficiently abstract and precise models, one cannot communicate the idea behind many aspects of software clearly and unambiguously.