skip to main content

Explore Research Products in the NSF-PAR

Title: Transformation of TOCL Temporal Properties into OCL
Specifying and verifying the temporal properties of UML-based systems can be challenging. Although there exist some extensions of OCL to support the specification of temporal properties in UML-based notations, most of the approaches depend on using non-UML formal formalisms such as LTL, CTL, and CTL* while transforming the under-development UML models into non-UML model checking frameworks for verification. This approach introduces complexities and relies on techniques and tools that are not within the UML spectrum. In this paper, we show how TOCL (one OCL extension for temporal properties specification) can be transformed into OCL for verification purposes. Towards this end, we created a formal EBNF grammar for TOCL, based on which a parser and a MOF metamodel were generated for the language. Additionally, to facilitate the analysis of the TOCL properties, we formally defined transformation rules from TOCL metamodel to OCL metamodel using QVT. Finally, we validated the implementations of the transformation rules using USE.  more » « less
Award ID(s):
1950416
NSF-PAR ID:
10376474
Author(s) / Creator(s):
; ; ; ;
Date Published:
Journal Name:
MODELS'22: ACM / IEEE 25th International Conference on Model Driven Engineering Languages and Systems Workshops
Format(s):
Medium: X
Sponsoring Org:
National Science Foundation
More Like this
  1. ; ; ( , Theory and Practice of Logic Programming)
    null (Ed.)
    Abstract In this paper, we study the problem of formal verification for Answer Set Programming (ASP), namely, obtaining a formal proof showing that the answer sets of a given (non-ground) logic program P correctly correspond to the solutions to the problem encoded by P , regardless of the problem instance. To this aim, we use a formal specification language based on ASP modules, so that each module can be proved to capture some informal aspect of the problem in an isolated way. This specification language relies on a novel definition of (possibly nested, first order) program modules that may incorporate local hidden atoms at different levels. Then, verifying the logic program P amounts to prove some kind of equivalence between P and its modular specification. 
    more » « less
  2. ; ; ; ; ; ; ; ( , ACM Transactions on Embedded Computing Systems)

    Formal verification of cyber-physical systems (CPS) is challenging because it has to consider real-time and concurrency aspects that are often absent in ordinary software. Moreover, the software in CPS is often complex and low-level, making it hard to assure that a formal model of the system used for verification is a faithful representation of the actual implementation, which can undermine the value of a verification result. To address this problem, we propose a methodology for building verifiable CPS based on the principle that a formal model of the software can be derivedautomaticallyfrom its implementation. Our approach requires that the system implementation is specified inLingua Franca(LF), a polyglot coordination language tailored for real-time, concurrent CPS, which we made amenable to the specification of safety properties via annotations in the code. The program structure and the deterministic semantics of LF enable automatic construction of formal axiomatic models directly from LF programs. The generated models are automatically checked using Bounded Model Checking (BMC) by the verification engineUclid5using theZ3SMT solver. The proposed technique enables checking a well-defined fragment of Safety Metric Temporal Logic (Safety MTL) formulas. To ensure the completeness of BMC, we present a method to derive an upper bound on the completeness threshold of an axiomatic model based on the semantics of LF. We implement our approach in the LF Verifierand evaluate it using a benchmark suite with 22 programs sampled from real-life applications and benchmarks for Erlang, Lustre, actor-oriented languages, and RTOSes. The LF Verifiercorrectly checks 21 out of 22 programs automatically.

     
    more » « less
  3. ; ; ( , 2022 IEEE 30th International Requirements Engineering Conference (RE))
    Temporal Logic (TL) bridges the gap between natural language and formal reasoning in the field of complex systems verification. However, in order to leverage the expressivity entailed by TL, the syntax and semantics must first be understood—a large task in itself. This significant knowledge gap leads to several issues: (1) the likelihood of adopting a TL-based verification method is decreased, and (2) the chance of poorly written and inaccurate requirements is increased. In this ongoing work, we present the Pythonic Formal Requirements Language (PyFoReL) tool: a Domain-Specific Language inspired by the programming language Python to simplify the elicitation of TL-based requirements for engineers and non-experts. 
    more » « less
  4. ; ; ; ; ( , REUNS 2022: The 8th National Workshop for REU Research in Networking and Systems)
    In this work we present a process and a tool to apply formal methods in Internet of Things (IoT) applications using the Unified Modeling Language (UML). As there are no best practices to develop secured IoT systems, we have developed a plug-in tool that integrates a framework to validate UML software models and we present the design of a location-based IoT application as a use case for the validation tool. 
    more » « less
  5. ; ; ; ; ( , ACM/IEEE International Conference on Cyber-Physical Systems)
    Cyber-Physical Systems (CPS) are integrations of computation, networking, and physical processes. The autonomy and self-adaptation capabilities of CPS mark a significant evolution from traditional control systems. Machine learning significantly enhances the functionality and efficiency of Cyber-Physical Systems (CPS). Large Language Models (LLM), like GPT-4, can augment CPS’s functionality to a new level by providing advanced intelligence support. This fact makes the applications above potentially unsafe and thus untrustworthy if deployed to the real world. We propose a comprehensive and general assurance framework for LLM-enabled CPS. The framework consists of three modules: (i) the context grounding module assures the task context has been accurately grounded (ii) the temporal Logic requirements specification module forms the temporal requirements into logic specifications for prompting and further verification (iii) the formal verification module verifies the output of the LLM and provides feedback as a guideline for LLM. The three modules execute iteratively until the output of LLM is verified. Experiment results demonstrate that our assurance framework can assure the LLM-enabled CPS. 
    more » « less
  • Citation Formats
  • MLA
  • APA
  • Chicago
  • BibTeX
  • Save / Share this Record
  • Send to Email