Software certification is defined as the process of independently confirming that a system or component complies with its specified requirements and is acceptable for use. It consists of the following steps: (1) the software producer subjects her software to rigorous testing and submits for certification, among other documents, evidence that the software has been thoroughly verified, and (2) the certifier evaluates the completeness of the verification and confirms that the software meets its specifications. The certification process is typically a manual evaluation of thousands of pages of documents that the software producer submits. Moreover, most of the current certification techniques focus on certifying testing results, but there is an increase in using formal methods to verify software. Model checking is a formal verification method that systematically explores the entire execution state space of a software program to ensure that a property is satisfied in every program state. As the field of model checking matures, there is a growing interest in its use for verification. In fact, several industrial-sized software projects have used model checking for verification, and there has been an increased push for techniques, preferably automated, to certify model checking results. Motivated by these challenges in certification, we have developed a set of automated techniques to certify model-checking results. One technique, called search-carrying code (SCC), uses information collected by a model checker during the verification of a program to speed up the certification of that program. In SCC, the software producer's model checker performs an exhaustive search of a program's state space and creates a search script that acts as a certificate of verification. The certifier's model checker uses the search script to partition its search task into a number of smaller, roughly balanced tasks that can be distributed to parallel model checkers, thereby using parallelization to speed up certification. When memory resources are limited, the producer's model checker can reduce its memory requirements by caching only a subset of the model-checking-search results. Caching increases the likelihood that an SCC verification task runs to completion and produces a search script that represents the program's entire state space. The downside of caching is that it can result in an increase in search time. We introduce cost-based caching, that achieves an exhaustive search faster than existing caching techniques. Finally, for cases when an exhaustive search is not possible, we present a novel method for estimating the state-space coverage of a partial model checking run. The coverage estimation can help the certifier to determine whether the partial model-checking results are adequate for certification.

Software certification is defined as the process of independently confirming that a system or component complies with its specified requirements and is acceptable for use. It consists of the following steps: (1) the software producer subjects her software to rigorous testing and submits for certification, among other documents, evidence that the software has been thoroughly verified, and (2) the certifier evaluates the completeness of the verification and confirms that the software meets its specifications. The certification process is typically a manual evaluation of thousands of pages of documents that the software producer submits. Moreover, most of the current certification techniques focus on certifying testing results, but there is an increase in using formal methods to verify software. Model checking is a formal verification method that systematically explores the entire execution state space of a software program to ensure that a property is satisfied in every program state. As the field of model checking matures, there is a growing interest in its use for verification. In fact, several industrial-sized software projects have used model checking for verification, and there has been an increased push for techniques, preferably automated, to certify model checking results. Motivated by these challenges in certification, we have developed a set of automated techniques to certify model-checking results. One technique, called search-carrying code (SCC), uses information collected by a model checker during the verification of a program to speed up the certification of that program. In SCC, the software producer's model checker performs an exhaustive search of a program's state space and creates a search script that acts as a certificate of verification. The certifier's model checker uses the search script to partition its search task into a number of smaller, roughly balanced tasks that can be distributed to parallel model checkers, thereby using parallelization to speed up certification. When memory resources are limited, the producer's model checker can reduce its memory requirements by caching only a subset of the model-checking-search results. Caching increases the likelihood that an SCC verification task runs to completion and produces a search script that represents the program's entire state space. The downside of caching is that it can result in an increase in search time. We introduce cost-based caching, that achieves an exhaustive search faster than existing caching techniques. Finally, for cases when an exhaustive search is not possible, we present a novel method for estimating the state-space coverage of a partial model checking run. The coverage estimation can help the certifier to determine whether the partial model-checking results are adequate for certification.

No description available.

Submitted by Maicon Juliano Schmidt (maicons) on 2015-06-30T12:58:44Z No. of bitstreams: 1 Lizandra Bays dos Santos.pdf: 9244211 bytes, checksum: 5d2cbae0a96db72c10de129513e76403 (MD5) / Made available in DSpace on 2015-06-30T12:58:44Z (GMT). No. of bitstreams: 1 Lizandra Bays dos Santos.pdf: 9244211 bytes, checksum: 5d2cbae0a96db72c10de129513e76403 (MD5) Previous issue date: 2013-01-31 / CAPES - Coordenação de Aperfeiçoamento de Pessoal de Nível Superior / A qualidade do processo de desenvolvimento de software, somente, não garante a qualidade do produto que é desenvolvido, sendo necessário combinar técnicas de qualidade do processo e do produto. Existem diversos esforços na comunidade acadêmica e no mercado para de modelos de certificação de qualidade do processo, e observa-se uma lacuna no que tange à certificação de qualidade de produtos de software. Este trabalho o desenvolvimento de um sistema que visa dar suporte para a certificação de qualidade de produtos de software. Um framework de processo para certificação de produtos é apresentado, o qual é composto de um subprocesso de especialização do modelo de qualidade focado em riscos, um subprocesso de medição da qualidade e um sobprocesso de avaliação da qualidade. Para apoiar estes subprocessos, a arquitetura do sistema desenvolvido faz uso de ontologias para representar o conhecimento envolvido no modelo de qualidade e agentes de software para manipular os indivíduos nas ontologias. / The software development process quality does not assure product quality, being necessary to combine techniques of process quality and product quality. There are several efforts in the academic community and in the market for models of quality certification of the development process, so that there is a gap regarding the quality certification of the product developed. This work presents the development of a system that aims to support the certification of quality software products. A framework of product certification process is showed, which is composed of subprocesses of quality model specialization, quality measurement and quality assessment. To support these subprocesses, the developed system architecture uses ontologies to represent knowledge about the quality model and software agents for handling to individuals in the ontologies.

This Master's Thesis describes methods of software certification and development of airborne systems, focusing on software testing and verification during project's life cycle. Thesis includes also designed software verification plan for concrete application according to RTCA/DO-178B. Another part of thesis illustrates the exemplary realization of tests according to designed verification plan. At the close we describe the options of applying the designed verification plan and evaluation of its results.