Towards a formalization of viewpoints testing
Bibliographic record
Abstract
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.
Fetched live from OpenAlex and de-inverted. Abstracts are not stored in this database: the inverted indexes are 8.6 GB of the frame’s 9.3 GB of text, and the host has 13 GB free.
How this classification was reachedexpand
Full frame machine prediction
Teacher imitationNot calibrated prevalence, not ground truth. Human validation pending. The Gemma side is a direct model label for every work in the frame, read from the title-only record. The Codex side is a classifier learned from the 10,348 direct Codex labels and calibrated to design-weighted sample rates; fields without enough sample support carry no Codex call. Candidate is the union of the two sides; consensus is their intersection. These outputs are machine_predicted_unvalidated and are not human labels.
Distilled classifier scores by category (both heads)
| Category | Codex | Gemma |
|---|---|---|
| Metaresearch | 0.016 | 0.044 |
| Meta-epidemiology (narrow) | 0.001 | 0.003 |
| Meta-epidemiology (broad) | 0.001 | 0.004 |
| Bibliometrics | 0.003 | 0.002 |
| Science and technology studies | 0.002 | 0.011 |
| Scholarly communication | 0.008 | 0.013 |
| Open science | 0.006 | 0.008 |
| Research integrity | 0.003 | 0.010 |
| Insufficient payload (model declined to judge) | 0.004 | 0.001 |
Machine scores (provisional)
The two teacher heads of the student model, read on this work. A score orders the frame for review; it never asserts a category, and the validation status ships verbatim with every row.
Baseline scores from an immature model (maturity gate not passed, 7 training rounds). Scores rank; they never assert a category.
score_only:v0-immature-baseline · verbatim from the scoring run: score_only means the number may rank works, and no category label ships from itClassification
machine, unvalidatedMachine predicted; a candidate call from one source (direct Gemma or distilled Codex), not a consensus.
How this classification was reached, model by model and score by score, is at the end of the page under "How this classification was reached".