A Graphics Function Standard Specification Validator
- URL: http://arxiv.org/abs/2401.17599v1
- Date: Wed, 31 Jan 2024 04:54:17 GMT
- Title: A Graphics Function Standard Specification Validator
- Authors: Steven D. Fraser and Peter P. Silvester
- Abstract summary: A validation methodology is proposed and implemented for natural language software specifications of standard graphics functions.
Checks are made for consistency, completeness, and lack of ambiguity in data element and function descriptions.
- Score: 0.0
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: A validation methodology is proposed and implemented for natural language
software specifications of standard graphics functions. Checks are made for
consistency, completeness, and lack of ambiguity in data element and function
descriptions. Functions and data elements are maintained in a relational
database representation. The appropriate checks are performed by sequences of
database operations. The relational database manager INGRES was used to support
a prototype implementation of the proposed technique. The methodology supports
the development of a scenario-based prototype from the information available in
the specification. This permits various function sequences to be checked
without implementation of the environment specified. The application of a
prototype implementation of the proposed methodology to the specification of
the Graphics Kernel System (GKS) software package demonstrates the
practicability of the method. Several inconsistencies in GKS related to the
definition of data elements have been identified.
Related papers
- Annotating Control-Flow Graphs for Formalized Test Coverage Criteria [0.3277163122167433]
We show how to annotate a Control-Flow Graph with decision information inferred from the graph itself.
We have implemented our algorithms in a tool which we show can be applied to automatically annotate CFGs output from popular compilers.
arXiv Detail & Related papers (2024-07-04T20:13:03Z) - Evaluating LLM-driven User-Intent Formalization for Verification-Aware Languages [6.0608817611709735]
Dafny and F* provide means to formally specify and prove properties of programs.
There is no algorithmic way of ensuring the correctness of the user-intent formalization for programs.
arXiv Detail & Related papers (2024-06-14T06:52:08Z) - Towards an Enforceable GDPR Specification [49.1574468325115]
Privacy by Design (PbD) is prescribed by modern privacy regulations such as the EU's.
One emerging technique to realize PbD is enforcement (RE)
We present a set of requirements and an iterative methodology for creating formal specifications of legal provisions.
arXiv Detail & Related papers (2024-02-27T09:38:51Z) - An Interactive Empirical Approach to the Validation of Software Package
Specifications [0.0]
The validation process is based on consistency checks.
By means of scenarios, the customer will be able to interactively experience the specified system prior to its implementation.
arXiv Detail & Related papers (2024-01-31T04:49:04Z) - SpecGen: Automated Generation of Formal Program Specifications via Large Language Models [20.36964281778921]
SpecGen is a novel technique for formal program specification generation based on Large Language Models.
We evaluate SpecGen on two datasets, including the SV-COMP 279 benchmark and a manually constructed dataset.
arXiv Detail & Related papers (2024-01-16T20:13:50Z) - Code Models are Zero-shot Precondition Reasoners [83.8561159080672]
We use code representations to reason about action preconditions for sequential decision making tasks.
We propose a precondition-aware action sampling strategy that ensures actions predicted by a policy are consistent with preconditions.
arXiv Detail & Related papers (2023-11-16T06:19:27Z) - A General Verification Framework for Dynamical and Control Models via Certificate Synthesis [54.959571890098786]
We provide a framework to encode system specifications and define corresponding certificates.
We present an automated approach to formally synthesise controllers and certificates.
Our approach contributes to the broad field of safe learning for control, exploiting the flexibility of neural networks.
arXiv Detail & Related papers (2023-09-12T09:37:26Z) - Measuring Rule-based LTLf Process Specifications: A Probabilistic
Data-driven Approach [2.5407767658470726]
Declarative process specifications define the behavior of processes by means of rules based on Linear Temporal Logic on Finite Traces.
In a mining context, these specifications are inferred from, and checked on, multi-sets of runs recorded by information systems.
We propose a technique that measures the degree of satisfaction of specifications over event logs.
arXiv Detail & Related papers (2023-05-09T13:07:01Z) - Relational Action Bases: Formalization, Effective Safety Verification,
and Invariants (Extended Version) [67.99023219822564]
We introduce the general framework of relational action bases (RABs)
RABs generalize existing models by lifting both restrictions.
We demonstrate the effectiveness of this approach on a benchmark of data-aware business processes.
arXiv Detail & Related papers (2022-08-12T17:03:50Z) - SMT-Based Safety Verification of Data-Aware Processes under Ontologies
(Extended Version) [71.12474112166767]
We introduce a variant of one of the most investigated models in this spectrum, namely simple artifact systems (SASs)
This DL, enjoying suitable model-theoretic properties, allows us to define SASs to which backward reachability can still be applied, leading to decidability in PSPACE of the corresponding safety problems.
arXiv Detail & Related papers (2021-08-27T15:04:11Z) - CoCoMoT: Conformance Checking of Multi-Perspective Processes via SMT
(Extended Version) [62.96267257163426]
We introduce the CoCoMoT (Computing Conformance Modulo Theories) framework.
First, we show how SAT-based encodings studied in the pure control-flow setting can be lifted to our data-aware case.
Second, we introduce a novel preprocessing technique based on a notion of property-preserving clustering.
arXiv Detail & Related papers (2021-03-18T20:22:50Z)
This list is automatically generated from the titles and abstracts of the papers in this site.
This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.