An environment for Ada software development based on formal specification

1987 ◽  
Vol VII (3) ◽  
pp. 94-106 ◽  
Author(s):  
D C Luckham ◽  
R Neff ◽  
D S Rosenblum
2010 ◽  
Vol 45 ◽  
Author(s):  
John A Van der Poll

An integration of traditional verification techniques and formal specifications in software engineering is presented. Advocates of such techniques claim that mathematical formalisms allow them to produce quality, verifiably correct, or at least highly dependable software and that the testing and maintenance phases are shortened. Critics on the other hand maintain that software formalisms are hard to master, tedious to use and not well suited for the fast turnaround times demanded by industry. In this paper some popular formalisms and the advantages of using these during the early phases of the software development life cycle are presented. Employing the Floyd-Hoare verification principles during the formal specification phase facilitates reasoning about the properties of a specification. Some observations that may help to alleviate the formal-methods controversy are established and a number of formal methods successes is presented. Possible conditions for an increased acceptance of formalisms in oftware development are discussed.


Author(s):  
MARTÍN LÓPEZ-NORES ◽  
JOSÉ J. PAZOS-ARIAS ◽  
JORGE GARCÍA-DUQUE ◽  
YOLANDA BLANCO-FERNÁNDEZ ◽  
REBECA P. DÍAZ-REDONDO ◽  
...  

Software development can be seen as a process of knowledge acquisition, in which human beings progressively learn about the intended behavior of the desired systems. Thereby, development is subject to considerable amounts of uncertainty and variability, that make it impossible to proceed in a purely incremental fashion — at some points, the need always arises to reconsider part of the accumulated knowledge. With this problem in mind, agile development methodologies have been gaining popularity in recent years as a means to enhance productivity, and there have been attempts to supplement them with formal techniques for better reliability. However, the existing approaches to agile formal methods have practically limited themselves to adopting recommended practices of agile development, with no particular contribution from the employed formalisms. Compared to that, this paper advocates the use of formalisms intended for evolutionary development, with a two-fold objective: first, to exploit the knowledge acquired up to any given stage as a means to cope with frequent and numerous changes; and, second, to introduce support for the creative development tasks through an interactive procedure that helps taking steps forward.


Author(s):  
Irfin Afifudi ◽  
Inge Martina

Designing process is inseparable from software development. Like other software development processes, designing process faces many problems, such as improper and ambiguous specifications. These problems may be overcome by applying formal engineering methods. One of which is Structured Object-Oriented Formal Language (SOFL). The analysis and formation of the design and implementation of SOFL are carried out as a solution to the problem. The application of SOFL is divided into three parts according to SOFL rules, namely informal specification, semi-formal specification, and formal specification. The design and implementation are measured and tested using rigorous review and maintainability index. This research uses a warehouse management system, a safety-critical system, as a case study. Rigorous analysis shows that SOFL in warehouse management system increases the maintainability index of 56.94%. It means that it is easier to develop.


Author(s):  
SHAOYING LIU ◽  
TETSUO TAMAI ◽  
SHIN NAKAJIMA

Software risk comes mainly from its poor reliability, but how to effectively achieve high reliability still remains a challenge. This paper puts forward a framework for systematically integrating formal specification, review, and testing, and shows how it can be applied to effectively eliminate errors in the major phases of software development process to enhance software reliability. In this framework, requirements errors can be removed and missing requirements can be identified by formalizing requirements into formal specifications whose validity can be ensured by rigorous review. The valid specification can then be used as a firm foundation for implementation and for rigorous inspection, testing, and walkthrough of the implemented program. We discuss how formalization, review, and testing work together at different levels of software development to improve software reliability through detecting and removing errors in documentation.


Sign in / Sign up

Export Citation Format

Share Document