Skip to main content
eScholarship
Open Access Publications from the University of California

Scholarly Works (6 results)

  • Thesis
  • Peer Reviewed
UC Berkeley Electronic Theses and Dissertations (2013)

Specification is the first and arguably the most important step for formal verification and correct-by-construction synthesis. These tasks require understanding precisely a design's intended behavior, and thus are only effective if the specification is created right. For example, much of the challenge in bug finding lies in finding the specification that mechanized tools can use to find bugs. It is extremely difficult to manually create a complete suite of good-quality formal specifications, especially given the enormous scale and complexity of designs today. Many real-world experiences indicate that poor or the lack of sufficient specifications can easily lead to misses of critical bugs, and in turn design re-spins and time-to-market slips.

This dissertation presents research that mitigates this manual and error-prone process through automation. The overarching theme is specification mining - the process of inferring likely specifications by observing a design's behaviors. We explore formalisms and algorithms to mine specifications from different sources, and demonstrate that the mined specifications are useful if not essential for a variety of applications such as verification, diagnosis and synthesis. The first part of the dissertation presents two approaches to mine specifications dynamically from simulation or execution traces. The first approach offers a simple but effective template-based remedy to the aforementioned problem. The second approach presents a novel formalism of specification mining based on the notion of sparse coding, which can learn latent structures in an unsupervised setting, and thus are not restricted by predefined templates. Additionally, we show that the mined specifications from both approaches can be used to localize bugs effectively.

In the second part of the dissertation, we study the problem of synthesis from temporal logic specifications. This synthesis approach offers an attractive proposition - one can automatically construct a functionally correct system from its behavioral description. The downside, however, is that it completely relies on the user to not only specify the intended behaviors of the system but also the assumptions on the environment. The latter is especially tricky in practice as environment assumptions are often implicit knowledge and seldom documented. We propose a framework that learns assumptions from the counterstrategies of an unrealizable specification to systematically guide it towards realizability. We further show that, the proposed counterstrategy-guided assumption mining approach enables the automatic synthesis of a new class of semi-autonomous controllers, called human-in-the-loop (HuIL) controllers. A crucial component of such a controller is an advisory that determines when to switch control from the autonomous controller to the human operator. We formalize the criteria that characterize a HuIL controller, by taking into account of human factors such as response time, and describe how to construct the advisory using assumption mining.

Human inputs are still critical in specification. In the last part of this dissertation, we describe two efforts on broadening the scope of specification mining with creative use of human inputs. The first is the design of a crowdsourced specification mining game called CrowdMine. The main idea of CrowdMine is to transform a design's traces into images and leverage the human ability to recognize patterns in images to assist the process of mining specifications. The second effort examines the feasibility of converting natural language specifications to formal specifications, with a focus on how specification mining encapsulated in a natural language processing (NLP) layer may assist non-expert users of formal methods at the requirement stage of a design.

    Cover page: Specification Mining: New Formalisms, Algorithms and Applications
    • Article
    • Peer Reviewed
    UC Davis Previously Published Works (2022)
    Inertial attitude estimation is a crucial component of many modern systems and applications. Attitude estimation from commercial-grade inertial sensors has been the subject of an abundance of research in recent years due to the proliferation of Inertial Measurement Units (IMUs) in mobile devices, such as the smartphone. Traditional methodologies involve probabilistic, iterative-state estimation; however, these approaches do not generalise well over changing motion dynamics and environmental conditions, as they require context-specific parameter tuning. In this work, we explore novel methods for attitude estimation from low-cost inertial sensors using a self-attention-based neural network, the Attformer. This paper proposes to part ways from the traditional cycle of continuous integration algorithms, and formulate it as an optimisation problem. This approach separates itself by leveraging attention operations to learn the complex patterns and dynamics associated with inertial data, allowing for the linear complexity in the dimension of the feature vector to account for these patterns. Additionally, we look at combining traditional state-of-the-art approaches with our self-attention method. These models were evaluated on entirely unseen sequences, over a range of different activities, users and devices, and compared with a recent alternate deep learning approach, the unscented Kalman filter and the iOS CoreMotion API. The inbuilt iOS had a mean angular distance from the true attitude of 117.31∘, the GRU 21.90∘, the UKF 16.38∘, the Attformer 16.28∘ and, finally, the UKF-Attformer had mean angular distance of 10.86∘. We show that this plug-and-play solution outperforms previous approaches and generalises well across different users, devices and activities.
      Cover page: Leveraging Self-Attention Mechanism for Attitude Estimation in Smartphones.Creative Commons 'BY' version 4.0 license
      • Article
      • Peer Reviewed
      UC Berkeley Previously Published Works (2017)
      A cyber-physical system (CPS) is an integration of computation with physical processes whose behavior is defined by both computational and physical parts of the system. In this paper, we present a view of the challenges and opportunities for design automation of CPS. We identify a combination of characteristics that define the challenges unique to the design automation of CPS. We then present selected promising advances in depth, focusing on four foundational directions: combining model-based and data-driven design methods; design for human-in-the-loop systems; component-based design with contracts, and design for security and privacy. These directions are illustrated with examples from two application domains: smart energy systems and next-generation automotive systems.
        Cover page: Design Automation of Cyber-Physical Systems: Challenges, Advances, and Opportunities
        • Article
        • Peer Reviewed
        UC Berkeley Previously Published Works (2013)
        We address the problem of verifying Probabilistic Computation Tree Logic (PCTL) properties of Markov Decision Processes (MDPs) whose state transition probabilities are only known to lie within uncertainty sets. We first introduce the model of Convex-MDPs (CMDPs), i.e., MDPs with convex uncertainty sets. CMDPs generalize Interval-MDPs (IMDPs) by allowing also more expressive (convex) descriptions of uncertainty. Using results on strong duality for convex programs, we then present a PCTL verification algorithm for CMDPs, and prove that it runs in time polynomial in the size of a CMDP for a rich subclass of convex uncertainty models. This result allows us to lower the previously known algorithmic complexity upper bound for IMDPs from co-NP to PTIME. We demonstrate the practical effectiveness of the proposed approach by verifying a consensus protocol and a dynamic configuration protocol for IPv4 addresses. © 2013 Springer-Verlag.
          • Article
          • Peer Reviewed
          UC Berkeley Previously Published Works (2013)
          Systems are increasingly being constructed from off-the-shelf components acquired through a globally distributed and untrusted supply chain. Often only post-synthesis gate-level netlists or actual silicons are available for security inspection. This makes reasoning about hardware trojans particularly challenging given the enormous scale of the problem. Currently, there is no mature methodology that can provide visibility into a bit-level design in terms of high-level components to allow more comprehensive analysis. In this paper, we present a systemic way of automatically deriving word-level structures from the gate-level netlist of a digital circuit. Our framework also provides the possibility for a user to specify sequences of word-level operations and it can extract the collection of gates corresponding to those operations. We demonstrate the effectiveness of our approach on a system-on-a-chip (SoC) design consisting of approximately 400,000 IBM 12SOI cells and several open-source designs. © 2013 IEEE.
            • Article
            • Peer Reviewed
            UC Santa Barbara Previously Published Works (2017)
            Many semi-distributed models that simulate pollutants' losses from watersheds do not handle well detailed spatially distributed and temporal data with which to identify accurate and cost-effective strategies for controlling pollutants issuing from non-point sources. Such models commonly overlook the flow pathways of pollutants across the landscape. This work aims at closing such knowledge gap by developing a Spatially and Temporally Distributed Empirical model for Phosphorus Management (STEM-P) that simulates the daily phosphorus loss from source areas to receiving waters on a spatially-distributed grid-cell basis. STEM-P bypasses the use of complex mechanistic algorithms by representing the phosphorus mobilization and delivery processes with zero-order mobilization and first-order delivery, respectively. STEM-P was applied to a 217km2 watershed with mixed forest and agricultural land uses situated in southwestern China. The STEM-P simulation of phosphorus concentration at the watershed outlet approximated the observed data closely: the percent bias (Pbias) was -7.1%, with a Nash-Sutcliffe coefficient (ENS) of 0.80 on a monthly scale for the calibration period. The Pbias was 18.1%, with a monthly ENS equal to 0.72 for validation. The simulation results showed that 76% of the phosphorus load was transported with surface runoff, 25.2% of which came from 3.4% of the watershed area (classified as standard A critical source areas), and 55.3% of which originated from 17.1% of the watershed area (classified as standard B critical source areas). The standard A critical source areas were composed of 51% residences, 27% orchards, 18% dry fields, and 4% paddy fields. The standard B critical source areas were mainly paddy fields (81%). The calculated spatial and temporal patterns of phosphorus loss and recorded flow pathways identified with the STEM-P simulations revealed the field-scale critical source areas and guides the design and placement of effective practices for non-point source pollution control and water quality conservation.
              Cover page: Evaluating the risk of phosphorus loss with a distributed watershed model featuring zero-order mobilization and first-order delivery
              Top