I work on rigorous systems engineering. Sound theory and disciplined design methodologies were key to enable the electronics revolution. How can any design field benefit from these? My current focus is the development of algebraic frameworks and software packages to reason about global system properties through local knowledge of the properties of the elements comprising the system.
Pacti: Scaling Assume-Guarantee Reasoning for System Analysis and Design
Inigo Incer, Apurva Badithela, Josefine Graebener, Piergiuseppe Mallozzi, Ayush Pandey, Sheng-Jung Yu, Albert Benveniste, Benoit Caillaud, Richard M. Murray, Alberto Sangiovanni-Vincentelli, and Sanjit A. Seshia
arXiv preprint 2303.17751. Mar 2023.Contract-based design is a method to facilitate modular system design. While there has been substantial progress on the theory of contracts, there has been less progress on scalable algorithms for the algebraic operations in this theory. In this paper, we present: 1) principles to implement a contract-based design tool at scale and 2) Pacti, a tool that can efficiently compute these operations. We then illustrate the use of Pacti in a variety of case studies. Pacti can be found at www.pacti.org.A Grammar for the Representation of Unmanned Aerial Vehicles with 3D Topologies
Piergiuseppe Mallozzi, Hussein Sibai, Inigo Incer, Sanjit A Seshia, and Alberto Sangiovanni-Vincentelli
arXiv preprint 2302.13980. Feb 2023.We propose a context-sensitive grammar for the systematic exploration of the design space of the topology of 3D robots, particularly unmanned aerial vehicles. It defines production rules for adding components to an incomplete design topology modeled over a 3D grid. The rules are local. The grammar is simple, yet capable of modeling most existing UAVs as well as novel ones. It can be easily generalized to other robotic platforms. It can be thought of as a building block for any design exploration and optimization algorithm.Algorithms for Context-Aided Variable Elimination
Inigo Incer, Albert Benveniste, Richard M. Murray. Alberto Sangiovanni-Vincentelli, and Sanjit Seshia
Tech. Rep. UCB/EECS-2023-15. EECS Department, University of California, Berkeley. Jan 2023.Deriving system-level specifications from component specifications usually involves the elimination of variables that are not part of the interface of the top-level system. This paper presents algorithms for eliminating variables from formulas by computing refinements or abstractions of these formulas in a context. We discuss a connection between this problem and optimization and give efficient algorithms to compute refinements and abstractions of linear inequality constraints.From Interface Automata to Hypercontracts
Inigo Incer, Albert Benveniste, Alberto Sangiovanni-Vincentelli, and Sanjit Seshia
Raskin, JF., Chatterjee, K., Doyen, L., Majumdar, R. (eds). Principles of Systems Design: Essays Dedicated to Thomas A. Henzinger on the Occasion of His 60th Birthday. Dec 2022.de Alfaro and Henzinger's interface automata brought renewed vigor to the tasks of specifying software formally and reasoning about systems compositionally. The key ingredients to this approach were the separation of concerns between environment and implementation, a light-weight behavioral interface that enabled more comprehensive compatibility checks than those allowed by type checking, and the notion of optimistic composition of specifications. This new impetus helped launch a research program of formally analyzing and designing general cyber-physical systems compositionally, where contract-based design has been playing a fundamental role. In this paper, we discuss the path connecting interface automata to the theory of contracts, with a special emphasis on hypercontracts, a recent development of contract theory.Contract-Based Specification Refinement and Repair for Mission Planning
Piergiuseppe Mallozzi, Inigo Incer, Pierluigi Nuzzo, and Alberto Sangiovanni-Vincentelli
arXiv preprint arXiv:2211.11908. Nov 2022.We address the problem of modeling, refining, and repairing formal specifications for robotic missions using assume-guarantee contracts. We show how to model mission specifications at various levels of abstraction and implement them using a library of pre-implemented specifications. Suppose the specification cannot be met using components from the library. In that case, we compute a proxy for the best approximation to the specification that can be generated using elements from the library. Afterward, we propose a systematic way to either 1) search for and refine the `missing part' of the specification that the library cannot meet or 2) repair the current specification such that the existing library can refine it. Our methodology for searching and repairing mission requirements leverages the quotient, separation, composition, and merging operations between contracts.Hypercontracts
Inigo Incer, Albert Benveniste, Alberto Sangiovanni-Vincentelli, and Sanjit Seshia
NASA Formal Methods: 14th International Symposium, NFM 2022. Pasadena, CA, USA. May 2022.
arXiv preprint arXiv:2106.02449. May 2021.Contract theories have been proposed to formally support distributed and decentralized system design while ensuring safe system integration. We propose hypercontracts, a general model with a richer structure for its underlying model of components, subsuming simulation preorders. While general, the new model provides a richer algebra for its notions of refinement, parallel composition, and quotient. Further, it allows the introduction of new operations. Building on top of these foundations, we propose conic hypercontracts, which are still generic but come with a finite description.From Specification to Implementation: Assume-Guarantee Contracts for Synthetic Biology
Ayush Pandey*, Inigo Incer*, Alberto Sangiovanni-Vincentelli, and Richard M Murray
* Equal contribution.
bioRxiv 2022.04.08.487709. April 2022.We provide a new perspective on using formal methods to model specifications and synthesize implementations for the design of biological circuits. In synthetic biology, design objectives are rarely described formally. We present an assume-guarantee contract framework to describe biological circuit design objectives as formal specifications. In our approach, these formal specifications are implemented by circuits modeled by ordinary differential equations, yielding a design framework that can be used to design complex synthetic biological circuits at scale. We describe our approach using the design of a biological AND gate as a motivating, running example.The Algebra of Contracts
Inigo Incer
PhD Thesis. EECS Department, University of California, Berkeley. May 2022.PhD thesis on the algebraic aspects of assume-guarantee contracts. It contains a historical discussion of contracts, the known algebraic operations on contracts and ways in which this operations are related, the notion of contract actions, syntactic considerations for software support of contracts, and the theory of hypercontracts.The Cyber-Physical Immune System: Work-in-Progress
Bo Pang*, Ashank Verma*, Jingchao Zhou*, Inigo Incer, and Alberto Sangiovanni-Vincentelli
* Equal contribution.
International Conference on Embedded Software (EMSOFT '21). Online. Oct 2021.We propose a conceptual approach to securing cyber-physical systems (CPS): the Cyber-Physical Immune System (CPIS), a collection of hardware and software elements deployed on top of a conventional CPS. Inspired by its biological counterpart, the CPIS comprises an independent network of distributed computing units that collects data from the conventional CPS, utilizes data-driven techniques to identify threats, adapts to the changing environment, alerts the user of any threats or anomalies, and deploys threat-mitigation strategies.The Quotient in Preorder Theories
Inigo Incer, Leonardo Mangeruca, Tiziano Villa, and Alberto Sangiovanni-Vincentelli
International Symposium on Games, Automata, Logics, and Formal Verification. Brussels, Belgium. Sept 2020.Seeking the largest solution to an expression of the form Ax ≤ B is a common task in several domains of engineering and computer science. This largest solution is commonly called quotient. We introduce an algebraic structure called preorder heap (preheap) which enables the closed-form expression of quotients. If solving Ax ≤ B is relevant to your application, check whether your theory is a preheap; if so, you immediately have a quotient.Coherent Extension, Composition, and Merging Operators in Contract Models for System Design
Roberto Passerone, Inigo Incer, and Alberto Sangiovanni-Vincentelli
ACM Trans. Embed. Comput. Syst. 18, 5s, Article 86. Oct 2019.
International Conference on Embedded Software (EMSOFT '19). New York, NY. Oct 2019.Contract models have been proposed to promote and facilitate reuse and distributed development. In this paper, we cast contract models into a coherent formalism used to derive general results about the properties of their operators. We study several extensions of the basic model, including the distinction between weak and strong assumptions and maximality of the specification. We then analyze the disjunction and conjunction operators, and show how they can be broken up into a sequence of simpler operations. This leads to the definition of a new contract viewpoint merging operator, which better captures the design intent in contrast to the more traditional conjunction. The adjoint operation, which we call separation, can be used to re-partition the specification into different viewpoints. We show the symmetries of these operations with respect to composition and quotient.Reactors: A Deterministic Model for Composable Reactive Systems
Marten Lohstroh, Inigo Incer, Andrés Goens, Patricia Derler, Jeronimo Castrillon, Edward A. Lee, and Alberto Sangiovanni-Vincentelli
Model-Based Design of Cyber Physical Systems (CyPhy'19). New York, NY. Oct 2019This paper describes a component-based concurrent model of computation for reactive systems. The components in this model, featuring ports and hierarchy, are called reactors. The model leverages a semantic notion of time, an event scheduler, and a synchronous-reactive style of communication to achieve determinism. Reactors enable a programming model that ensures determinism, unless explicitly abandoned by the programmer. We show how the coordination of reactors can safely and transparently exploit parallelism, both in shared-memory and distributed systems.A Metric for Linear Temporal Logic
Inigo Incer, Marten Lohstroh, Antonio Iannopollo, Edward A. Lee, and Alberto Sangiovanni-Vincentelli
arXiv preprint arXiv:1812.03923. Oct 2018.We propose a measure and a metric on the sets of infinite traces generated by a set of atomic propositions. To compute these quantities, we first map properties to subsets of the real numbers and then take the Lebesgue measure of the resulting sets. We analyze how this measure is computed for Linear Temporal Logic (LTL) formulas. An implementation for computing the measure of bounded LTL properties is provided and explained. This implementation leverages SAT model counting and effects independence checks on subexpressions to compute the measure and metric compositionally.Quotient for Assume-Guarantee Contracts
Inigo Incer, Alberto Sangiovanni-Vincentelli, Chung-Wei Lin, and Eunsuk Kang
16th ACM-IEEE International Conference on Formal Methods and Models for System Design (MEMOCODE ’18). Beijing, China.The algebra of assume-guarantee (AG) contracts was introduced to provide technical counterparts to the legal commitments between parties in a supply chain. It was not known whether the AG algebra had a notion of quotient, i.e., the adjoint of composition. This paper settles that question in the affirmative, and provides a closed-form expression for the quotient.Adversarially Robust Malware Detection Using Monotonic Classification
Inigo Incer*, Michael Theodorides*, Sadia Afroz, and David Wagner
* Equal contribution.
ACM International Workshop on Security and Privacy Analytics (IWSPA '18). Tempe, AZ.
Coverage: Microsoft Defender ATP Research Team, WinBuzzerWe propose monotonic classification with selection of monotonic features as a defense against evasion attacks on classifiers for malware detection. The monotonicity property of our classifier ensures that an adversary will not be able to evade the classifier by adding more features. We train and test our classifier on over one million executables collected from VirusTotal.
Microsoft implemented our proposed mechanism in its Defender ATP, and the technique was key in stopping the LockerGoga ransomware. The coverage links provide more information.