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

• Consistency Verification in Ontology-Based Process Models with Parameter Interdependencies [40.539768677361735]
  Formalization of process knowledge enables consistent modeling of parameter interdependencies in manufacturing.<n>To support cross-context application and knowledge reuse, such expressions are defined in a generic form and applied across multiple process contexts.<n>This paper presents a set of verification mechanisms for a previously developed process semantics-based model.
  arXiv  Detail & Related papers  (2025-06-19T07:21:16Z)
• What is Formal Verification without Specifications? A Survey on mining LTL Specifications [5.655251163654288]
  We list and compare advances in mining specifications in Linear Temporal Logic (LTL), the de facto standard specification language for reactive systems. Several approaches have been designed for learning formulas, which address different aspects and settings of specification design. We survey the current state-of-the-art techniques and compare them for the convenience of the formal methods practitioners.
  arXiv  Detail & Related papers  (2025-01-27T18:06:48Z)
• Evaluating the Ability of Large Language Models to Generate Verifiable Specifications in VeriFast [5.019791860882564]
  This paper explores OpenAI's GPT-4o model's effectiveness in generating specifications on C programs that are verifiable with VeriFast. Our results indicate that the specifications generated by GPT-4o preserve functional behavior, but struggle to be verifiable.
  arXiv  Detail & Related papers  (2024-11-04T17:44:11Z)
• 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)
• 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)
• Rely-guarantee Reasoning about Concurrent Memory Management: Correctness, Safety and Security [0.0]
  An incorrect specification and implementation of the memory management may lead to system crashes or exploitable attacks. This article presents the first formal specification and mechanized proof of a concurrent memory management for a real-world OS.
  arXiv  Detail & Related papers  (2023-09-17T03:41:10Z)
• A General Framework for Verification and Control of Dynamical 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.