Towards a formalization of viewpoints testing
Notice bibliographique
Résumé
Testing is an important technique for validating and checking the correctness of software.However, the production and application of effective and efficient tests is typically extremely difficult, expensive, laborious, error-prone and time consuming.Formal methods are a way of specifying and verifying software systems by applying techniques from mathematics and logic.This enables the developer to analyze system models and reason about them with mathematical precision and rigour.Thus both formal methods and software testing can be used to improve software quality.Traditionally, formal methods and testing have been seen as rival approaches.However, in recent years a new consensus has developed.Under this consensus, formal methods and testing are seen as complementary.In particular, it has been shown that the presence of a formal specification can assist the test process in a number of ways.The specification may act as an oracle or as the basis for systematic, and possibly automatic, test synthesis.In conjunction with test hypotheses or a fault model, formal specifications have also been used to allow stronger statements, about test effectiveness, to be made.It is possible that the contribution to testing will be one of the main benefits of using formal methods.The aim of the workshop FATES -Formal Approaches to Testing of Software -is to be a forum for researchers, developers and testers to present ideas about and discuss the use of formal methods in software testing.Topics of interest are formal test theory, test tools and applications of testing based on formal methods, including algorithmic generation of tests from formal specifications, test result analysis, test selection and coverage computation based on formal models, and all of this based on different formal methods, and applied in different application areas.This volume contains the papers presented at FATES'02 which was held in Brno (Czech Republic) on August 24, 2002, as an affiliated workshop of CONCUR'02.Out of 17 submitted papers the programme committee selected 9 regular papers and 1 position paper for presentation at the workshop.Together with the keynote presentation by Elaine Weyuker, from AT& T Labs, USA, they form the contents of these proceedings.The papers present different approaches to using formal methods in software testing.The main theme is the generation of an efficient and effective set of test cases from a formal description.Different models and formalisms are used as the starting point, such as (probabilistic) finite state machines, X-machines, transition systems, iii categories, B, Z, Statecharts, UML, and different methodologies and algorithms are discussed for the test derivation process, ranging from formalization of the manual testing process to the (re)use of techniques from model checking.The papers give insight in what has been achieved in the area of software testing with formal methods.Besides, they give clear indications of what has to be done before we can expect widespread use of formal techniques in software testing.The prospects for using formal methods to improve the quality and reduce the cost of software testing are good, but still more effort is needed, both in developing new theories and in making the existing methods and theories applicable, e.g., by providing tool support.We would like to thank the programme committee and the additional reviewers for their support in selecting and composing the workshop programme, and we thank the authors for their contributions without which, of course, these proceedings would not exist.
Récupéré en direct depuis OpenAlex et désinversé. Les résumés ne sont pas conservés dans cette base de données : les index inversés représentent 8,6 Go des 9,3 Go de texte de la base, et le serveur dispose de 13 Go libres.
Comment cette classification a été obtenuedéplier
Prédiction machine sur la base complète
Imitation des enseignantsNi prévalence calibrée, ni vérité terrain. Validation humaine à venir. Le volet Gemma est une étiquette directe du modèle pour chaque travail de la base, lue sur la notice réduite au titre. Le volet Codex est un classifieur appris des 10 348 étiquettes directes de Codex et calibré sur les taux pondérés de l'échantillon; les champs sans appui suffisant ne portent aucun appel Codex. Le mode candidate est l'union des deux volets; le consensus est leur intersection. Ces sorties portent le statut machine_predicted_unvalidated et ne sont pas des étiquettes humaines.
Scores du classifieur distillé par catégorie (deux têtes)
| Catégorie | Codex | Gemma |
|---|---|---|
| Métarecherche | 0,016 | 0,044 |
| Méta-épidémiologie (sens strict) | 0,001 | 0,003 |
| Méta-épidémiologie (sens large) | 0,001 | 0,004 |
| Bibliométrie | 0,003 | 0,002 |
| Études des sciences et des technologies | 0,002 | 0,011 |
| Communication savante | 0,008 | 0,013 |
| Science ouverte | 0,006 | 0,008 |
| Intégrité de la recherche | 0,003 | 0,010 |
| Charge utile insuffisante (le modèle a refusé de juger) | 0,004 | 0,001 |
Scores machine (provisoires)
Les deux têtes enseignantes du modèle étudiant, lues sur ce travail. Un score ordonne la base pour la relecture; il n'affirme jamais une catégorie, et le statut de validation accompagne chaque rangée tel quel.
Scores de référence d'un modèle non mature (critères de maturité non atteints, 7 itérations). Un score ordonne; il n'affirme jamais une catégorie.
score_only:v0-immature-baseline · tel quel depuis la passe de notation : score_only signifie que le nombre peut ordonner les travaux, et qu'aucune étiquette de catégorie n'en découleClassification
machine, non validéePrédiction automatique; un appel candidat d’une seule source (Gemma direct ou Codex distillé), pas un consensus.
Le détail, modèle par modèle et score par score, se trouve en fin de page sous « Comment cette classification a été obtenue ».