/software_verification

Software testing and verification scripts.

Primary LanguagePython

Software testing scripts

This repository contains few small scripts, which may be useful for generating test cases.

Def-use paths

Given a control flow digraph (constructed from a piece of code) with some nodes designated as defs or uses, this script constructs all def-clear paths between each du-pair. For details, see Paul Ammann, Jeff Offutt, "Introduction to Software Testing" (2017).

To run, enter du_paths/, enter desired graph as a list of directed edges, def and use node in du_paths.py and run

python3.6 du_paths.py.

The output is in the form of

du(start_node, end_node, variable_name) = list_of_paths.

Prime paths

A path between two digraph nodes is considered a prime path iff it is a simple path and it does not appear as a proper subpath of any other simple path. The model.py script in model/ prime path coverage (a set containing all prime paths) for a graph given as a list of directed edges. For details, see Paul Ammann, Jeff Offutt, "Introduction to Software Testing" (2017).

To run:

cd model/ python3.6 model.

The output is subpaths considered in the individual steps of the algorithm, the resulting paths, and LaTeX formatted paths. ! signifies a prime path, * a cycle.

Mutually orthogonal latin squares and orthogonal arrays

For every prime power p, there exists p-1 so called mutually orthogonal latin squares. Each latin square has the property that for each row or column no element is present more than once. For each two mutually orthogonal latin squares, it is the case that each pair of elements with the same coordinates appear exactly once.

Orthogonal arrays are a generalization of latin squares into a tabular form. For orthogonal array of strength s, for each s-tuple of columns, each corresponding row elements appear exactly once (or, in general, the same number of times).

os.py in tbl2txt converts a given orthogonal array and an array of factors (possible parameter values) the values of factors for tests generated by the orthogonal square.

ls.py does the same, but given a list of orthogonal squares.

Alloy

Alloy is a powerful declarative model-based language and tool for software modelling and verification. It allows efficient construction of software models, subsequent constraint definition and verification of constraint satisfaction.

alloy/ contains my Alloy solution, langdon.als, to a puzzle presented in 6_langdon.pdf. To run it, please open and execute in Alloy Analyzer.

Moreover, 6_clanek.pdf is my report on the mondex study, and prezentace.pdf is a corresponding presentation.