This page collects journal articles, conference papers, book chapters, and technical reports. Search by title, author, venue, year, or publication type. Select Abstract or BibTeX to expand either one without leaving the page.
2026
Early design exploration of aerospace systems using assume–guarantee contracts
Nicolas Rouquette, Alessandro Pinto, Inigo Incer
Journal of Aerospace Information SystemsJournal article
Abstract
We present a compositional approach to the early modeling and analysis of complex aerospace systems based on assume–guarantee contracts. Components in a system are abstracted into assume–guarantee specifications. Performing algebraic contract operations with Pacti allows us to relate local component specifications to those of the system. Applications to two aerospace case studies—the design of spacecraft to satisfy a rendezvous mission and the design of the thermal management system of a prototypical aircraft—show that this methodology provides engineers with an agile, early analysis and exploration process. We show that the analysis of thousands of configurations can be achieved on the order of seconds to minutes on a consumer-grade CPU.
BibTeX
@article{rouquette_early_2026,
author = {Rouquette, Nicolas and Pinto, Alessandro and Incer, Inigo},
title = {Early Design Exploration of Aerospace Systems Using
Assume–Guarantee Contracts},
journal = {Journal of Aerospace Information Systems},
volume = {23},
number = {9},
pages = {820-835},
date = {2026},
doi = {10.2514/1.I011529}
}
DOI
2026
Stochastic programming for uncertainty-aware global lunar path planning
Garrett R Schueller, John-Paul Clarke, Alessandro Pinto
ASCEND 2026Book chapter
BibTeX
@inbook{schueller2026stochastic,
author = {Schueller, Garrett R and Clarke, John-Paul and Pinto,
Alessandro},
title = {Stochastic Programming for Uncertainty-Aware Global Lunar
Path Planning},
booktitle = {ASCEND 2026},
date = {2026}
}
2026
LLM-assisted translation and bounded model checking of python code
Shivkumar Shivaji, Natalia Lobakhina, Klaus Havelund, Alessandro Pinto, Lucas Cordeiro
3rd artificial intelligence ISoLABook chapter
BibTeX
@inbook{shivaji2026llm,
author = {Shivaji, Shivkumar and Lobakhina, Natalia and Havelund,
Klaus and Pinto, Alessandro and Cordeiro, Lucas},
title = {LLM-Assisted Translation and Bounded Model Checking of Python
Code},
booktitle = {3rd artificial intelligence ISoLA},
date = {2026}
}
2026
Ensemble rollout decision making for uncertainty-aware aircraft routing
Garrett R Schueller, John-Paul Clarke, Alessandro Pinto
AIAA AVIATION 2026 forumConference paper
BibTeX
@inproceedings{schueller2026ensemble,
author = {Schueller, Garrett R and Clarke, John-Paul and Pinto,
Alessandro},
title = {Ensemble Rollout Decision Making for Uncertainty-Aware
Aircraft Routing},
booktitle = {AIAA AVIATION 2026 forum},
pages = {4013},
date = {2026}
}
2026
An engineering life-cycle assurance process for autonomous space systems
Alessandro Pinto, Caleb Wagner, Klaus Havelund, Nicolas Rouquette
IEEE aerospace conferenceConference paper
BibTeX
@inproceedings{pinto_paas_2026,
author = {Pinto, Alessandro and Wagner, Caleb and Havelund, Klaus and
Rouquette, Nicolas},
title = {An Engineering Life-Cycle Assurance Process for Autonomous
Space Systems},
booktitle = {IEEE aerospace conference},
date = {2026}
}
2026
Robust verification of controllers under state uncertainty via hamilton-jacobi reachability analysis
Albert Lin, Alessandro Pinto, Somil Bansal
SubmittedConference paper
BibTeX
@inproceedings{lin_robust_verification_2026,
author = {Lin, Albert and Pinto, Alessandro and Bansal, Somil},
title = {Robust Verification of Controllers Under State Uncertainty
via Hamilton-Jacobi Reachability Analysis},
booktitle = {Submitted},
date = {2026}
}
2025
Analyzing lunar imagery using computer vision models to improve path planning
Garrett R Schueller, John-Paul Clarke, Alessandro Pinto
AIAA AVIATION FORUM AND ASCEND 2025Conference paper
Abstract
Accurate global path planning is critical to the success of lunar rover missions, yet current approaches are fundamentally constrained by uncertainty in remote sensing data. Orbital imagery provides only partial and low-resolution information about surface hazards, rendering deterministic planning strategies brittle to unexpected terrain conditions. To address this challenge, we propose a method for generating probabilistic terrain models suitable for stochastic optimization. A convolutional neural network classifier is trained on lunar imagery to predict traversability distributions across surface regions, enabling the construction of uncertainty-aware cost maps. Testing shows that the model performs well, significantly surpassing traditional image processing techniques and human performance at the classification task. To better capture realistic terrain variability, spatial correlations between adjacent regions are incorporated into the sampling process. These uncertainty-aware maps can be sampled to generate coherent terrain realizations, providing inputs to two-stage stochastic programming models for robust global path planning under uncertainty.
BibTeX
@inproceedings{schueller2025analyzing,
author = {Schueller, Garrett R and Clarke, John-Paul and Pinto,
Alessandro},
title = {Analyzing Lunar Imagery Using Computer Vision Models to
Improve Path Planning},
booktitle = {AIAA AVIATION FORUM AND ASCEND 2025},
pages = {4028},
date = {2025}
}
Paper
2025
Contract embeddings for layered control architectures
Nikhil Vijay Naik, Alessandro Pinto, Pierluigi Nuzzo
ACM Trans. Embed. Comput. Syst.Journal article
Abstract
The design of complex cyber-physical system architectures is often hierarchical. System specifications are mapped to an implementation layer via a stepwise refinement process involving multiple intermediate layers. These layers may capture different functionalities, and the orchestration of a variety of heterogeneous techniques suited to each layer may be required to achieve the overall design objectives. Due to their heterogeneity, ensuring traceability and verifiability of such architectures is a challenging problem. In this article, we present a correct-by-construction methodology for designing heterogeneous layered architectures. We capture the specifications at each layer with assume-guarantee contracts, a specification paradigm which can encompass a variety of modeling formalisms. We then use the notion of contract embeddings to define specification refinement, rigorously and traceably mapping specifications across layers modeled with heterogeneous formalisms. We instantiate our methodology on the design of layered control architectures (LCAs), resulting in a novel approach that can verifiably orchestrate domain-specific techniques to satisfy both global planning and local safety requirements. In the context of LCAs, we derive necessary conditions for correct specification refinement and results for compositional realization of control safety specifications. We illustrate our design methodology on a motivating example and a case study derived from robotic mission planning and control.
BibTeX
@article{naik_lca_tecs2025,
author = {Naik, Nikhil Vijay and Pinto, Alessandro and Nuzzo,
Pierluigi},
publisher = {Association for Computing Machinery},
title = {Contract Embeddings for Layered Control Architectures},
journal = {ACM Trans. Embed. Comput. Syst.},
volume = {24},
number = {5s},
date = {2025-09},
address = {New York, NY, USA},
url = {https://doi.org/10.1145/3764587},
doi = {10.1145/3764587},
issn = {1539-9087}
}
DOI
Paper
2024
Contract-Based Hierarchical Modeling and Traceability of Heterogeneous Requirements
Nikhil Vijay Naik, Alessandro Pinto, Pierluigi Nuzzo
IEEE Transactions on Computer-Aided Design of Integrated Circuits and SystemsJournal article
Abstract
The design of complex mission-critical systems often follows a layered approach, which may lead to complicated, multilevel, multiviewpoint requirement hierarchies. This heterogeneity makes it challenging to guarantee the traceability of the requirements across levels of abstraction and, consequently, the satisfaction of the requirements by a system implementation, especially when requirements at different abstraction levels are expressed using different mathematical formalisms and modeling languages. In this article, we address this challenge by introducing heterogeneous hierarchical contract networks (HHCNs), a formal model based on a graph of assume-guarantee contracts, for capturing and analyzing heterogeneous requirement hierarchies. We formulate the requirement traceability validation problem in terms of contract refinement relations between nodes in an HHCN. We then define contract embeddings to enable reasoning about refinements across levels of abstraction in the HHCN that are expressed using heterogeneous formalisms. Contract embeddings leverage the notion of conservative approximation to rigorously map contracts across levels of abstraction while ensuring that refinement is preserved independently of the formalism to which the contracts are mapped. We illustrate their effectiveness on a case study motivated by a multiagent autonomous lunar rover mission.
BibTeX
@article{naik_contract-based_2024,
author = {Naik, Nikhil Vijay and Pinto, Alessandro and Nuzzo,
Pierluigi},
publisher = {IEEE},
title = {Contract-Based {Hierarchical} {Modeling} and {Traceability}
of {Heterogeneous} {Requirements}},
journal = {IEEE Transactions on Computer-Aided Design of Integrated
Circuits and Systems},
date = {2024}
}
Paper
2024
Learning Hierarchical Control For Constrained Dynamic Task Assignment
Charlott Vallon, Alessandro Pinto, Bartolomeo Stellato, Francesco Borrelli
2024 63rd IEEE Conference on Decision and Control (CDC)Conference paper
BibTeX
@inproceedings{vallon_learning_2024,
author = {Vallon, Charlott and Pinto, Alessandro and Stellato,
Bartolomeo and Borrelli, Francesco},
title = {Learning {Hierarchical} {Control} {For} {Constrained}
{Dynamic} {Task} {Assignment}},
booktitle = {2024 63rd IEEE Conference on Decision and Control (CDC)},
date = {2024}
}
2024
Learning Hierarchical Control Systems for Autonomous Systems with Energy Constraints
Charlott Vallon, Mark Pustilnik, Alessandro Pinto, Francesco Borrelli
2024 63rd IEEE Conference on Decision and Control (CDC)Conference paper
Abstract
This paper focuses on the design of hierarchical control architectures for autonomous systems with energy constraints. We focus on systems where energy storage limitations and slow recharge rates drastically affect the way the autonomous systems are operated. Using examples from space robotics and public transportation, we motivate the need for formally designed learning hierarchical control systems. We propose a learning control architecture which incorporates learning mechanisms at various levels of the control hierarchy to improve performance and resource utilization. The proposed hierarchical control scheme relies on high-level energy-aware task planning and assignment, complemented by a low-level predictive control mechanism responsible for the autonomous execution of tasks, including motion control and energy management. Simulation examples show the benefits and the limitations of the proposed architecture when learning is used to obtain a more energy-efficient task allocation.
BibTeX
@inproceedings{vallon_learning_2024_1,
author = {Vallon, Charlott and Pustilnik, Mark and Pinto, Alessandro
and Borrelli, Francesco},
title = {Learning {Hierarchical} {Control} {Systems} for {Autonomous}
{Systems} with {Energy} {Constraints}},
booktitle = {2024 63rd IEEE Conference on Decision and Control (CDC)},
date = {2024}
}
Paper
2023
Survey of human models for verification of human-machine systems
Timothy E Wang, Alessandro Pinto
arXivedJournal article
Abstract
We survey the landscape of human operator mod- eling ranging from the early cognitive models developed in artificial intelligence to more recent formal task models developed for model-checking of human machine interactions. We review human performance modeling and human factors studies in the context of aviation, and models of how the pilot interacts with automation in the cockpit. The purpose of the survey is to assess the applicability of available state-of-the-art models of the human operators for the design, verification and validation of future safety-critical aviation systems that exhibit higher-level of autonomy, but still require human operators in the loop. These systems include the single-pilot aircraft and NextGen air traffic management. We discuss the gaps in existing models and propose future research to address them.
BibTeX
@article{wang2023survey,
author = {Wang, Timothy E and Pinto, Alessandro},
title = {Survey of Human Models for Verification of Human-Machine
Systems},
journal = {arXived},
date = {2023},
url = {https://arxiv.org/abs/2307.15082}
}
Paper
Publisher
2023
Aace: Automated assurance case environment for aerospace certification
Zamira Daw, Chanwook Oh, Matthew Low, Timothy Wang, Isaac Amundson, Alessandro Pinto, Massimiliano Chiodo, Guoqiang Wang, Saqib Hasan, Ryan Melville, others
2023 IEEE/AIAA 42nd Digital Avionics Systems Conference (DASC)Conference paper
Abstract
A certification process evaluates whether the risk of a system is acceptable for its intent. Certification processes are complex and usually human-driven, requiring expert evaluators to determine software conformance to certification guidelines based on a large number of development artifacts. These processes may result in superficial, biased, and long evaluations. In this paper, we propose a computer-aided assurance framework, called Automated Assurance Case Environment (AACE), enabling synthesis and validation of assurance cases (ACs) based on a system's specification, assurance evidence, and domain expert knowledge captured in AC patterns. A commercial aerospace case study shows that the generated ACs are meaningful, and numerical results show the efficiency of AACE.
BibTeX
@inproceedings{daw_aace_2023,
author = {Daw, Zamira and Oh, Chanwook and Low, Matthew and Wang,
Timothy and Amundson, Isaac and Pinto, Alessandro and Chiodo,
Massimiliano and Wang, Guoqiang and Hasan, Saqib and Melville, Ryan
and {others}},
publisher = {IEEE},
title = {Aace: {Automated} Assurance Case Environment for Aerospace
Certification},
booktitle = {2023 IEEE/AIAA 42nd Digital Avionics Systems Conference
(DASC)},
pages = {1-10},
date = {2023}
}
Paper
2023
Computer-aided generation of assurance cases
Timothy E Wang, Chanwook Oh, Matthew Low, Isaac Amundson, Zamira Daw, Alessandro Pinto, Massimiliano L Chiodo, Guoqiang Wang, Saqib Hasan, Ryan Melville, others
International Conference on Computer Safety, Reliability, and SecurityConference paper
Abstract
Assurance cases (ACs) have gained attention in the aerospace, medical, and other heavily-regulated industries as a means for providing structured arguments on why a product is dependable (i.e., safe, secure, etc.) for its intended application. Challenges in AC construction stem from the complexity and uniqueness of the designs, the heterogeneous nature of the required supporting evidence, and the need to assess the quality of an argument. We present an automated AC generation framework that facilitates the construction, validation, and confidence assessment of ACs based on dependability argument pat- terns and confidence patterns capturing domain knowledge. The ACs are instantiated with a system’s specification and evaluated based on the available design and verification evidence. Aerospace case studies illustrate the framework’s effectiveness, efficiency, and scalability.
BibTeX
@inproceedings{wang_computer-aided_2023,
author = {Wang, Timothy E and Oh, Chanwook and Low, Matthew and
Amundson, Isaac and Daw, Zamira and Pinto, Alessandro and Chiodo,
Massimiliano L and Wang, Guoqiang and Hasan, Saqib and Melville,
Ryan and {others}},
publisher = {Springer},
title = {Computer-Aided Generation of Assurance Cases},
booktitle = {International Conference on Computer Safety, Reliability,
and Security},
pages = {135-148},
date = {2023}
}
2023
Early Design Exploration of Space System Scenarios Using Assume-Guarantee Contracts
Nicolas Rouquette, Inigo Incer, Alessandro Pinto
2023 IEEE 9th International Conference on Space Mission Challenges for Information Technology (SMC-IT)Conference paper
Abstract
We present a compositional approach to modeling and analyzing space mission operation sequences with steps across multiple viewpoints. We consider different operation tasks such as communication, science observation, trajectory correction, and battery charging; and separate their interactions across discipline viewpoints. In each sequence step, these tasks are modeled as assume-guarantee contracts. They make assumptions on the initial state of a step, and if these assumptions are satisfied, they guarantee desirable properties of the state at the end of the step. These models are then used in Pacti, a tool for reasoning about contracts. We demonstrate a design methodology leveraging Pacti's operations: contract composition for computing the contract for the end-to-end sequence of steps and contract merging for combining them across viewpoints. We also demonstrate applying Pacti's optimization techniques to analyze the figures of merit of admissible sequences satisfying operational requirements for a CubeSat-sized spacecraft performing a small-body asteroid rendez-vous mission. We show that analyzing tens of thousands of combinations of sequences and operational requirements takes just over one minute, confirming the scalability of the approach. The methodology presented in this paper supports the early design phases, including requirement engineering and task modeling.
BibTeX
@inproceedings{rouquette_early_2023,
author = {Rouquette, Nicolas and Incer, Inigo and Pinto, Alessandro},
publisher = {IEEE},
title = {Early {Design} {Exploration} of {Space} {System} {Scenarios}
{Using} {Assume-Guarantee} {Contracts}},
booktitle = {2023 IEEE 9th International Conference on Space Mission
Challenges for Information Technology (SMC-IT)},
pages = {15-24},
date = {2023}
}
2023
Assurance for Autonomy–JPL’s past research, lessons learned, and future directions
Martin S Feather, Alessandro Pinto
2023 IEEE International Conference on Assured Autonomy (ICAA)Conference paper
Abstract
Robotic space missions have long depended on automation, defined in the 2015 NASA Technology Roadmaps as "the automatically-controlled operation of an apparatus, process, or system using a pre-planned set of instructions (e.g., a command sequence), to react to events when a rapid response is required".Autonomy, defined there as "the capacity of a system to achieve goals while operating independently from external control," is required when a wide variation in circumstances precludes responses being pre-planned, instead autonomy follows an on-board deliberative process to determine the situation, decide the response, and manage its execution. Autonomy is increasingly called for to support adventurous space mission concepts, as an enabling capability or as a significant enhancer of the science value that those missions can return. But if autonomy is to be allowed to control these missions' expensive assets, all parties in the lifetime of a mission, from proposers through ground control, must have high confidence that autonomy will perform as intended to keep the asset safe to (if possible) accomplish the mission objectives. The role of mission assurance is a key contributor to providing this confidence, yet assurance practices honed over decades of spaceflight have relatively little experience with autonomy. To remedy this situation, researchers in JPL's software assurance group have been involved in the development of techniques specific to the assurance of autonomy. This paper summarizes over two decades of this research, and offers a vision of where further work is needed to address open issues.
BibTeX
@inproceedings{feather_assurance_2023,
author = {Feather, Martin S and Pinto, Alessandro},
publisher = {IEEE},
title = {Assurance for {Autonomy–JPL’s} Past Research, Lessons
Learned, and Future Directions},
booktitle = {2023 IEEE International Conference on Assured Autonomy
(ICAA)},
pages = {97-105},
date = {2023}
}
Paper
2023
Leveraging Compositional Methods for Modeling and Verification of an Autonomous Taxi System
Alessandro Pinto, Anthony Corso, Edward Schmerling
2023 IEEE International Conference on Assured Autonomy (ICAA)Conference paper
Abstract
The environments and the goals that an autonomous system needs to be able to understand and act upon are not fully known and clearly identifiable at design time, especially for those systems that interact with the physical world. Still, for applications that require a certain level of assurance, requirements, which include the definition of how a system is supposed to interact with its context, need to be defined, analyzed, refined towards an implementation that can be shown to deliver certain guarantees. We first broadly discuss the importance of the early stages of the design process where requirements are defined, and we then discuss the formalisms needed to capture requirements and refine them towards implementation for autonomous systems.
BibTeX
@inproceedings{pinto_leveraging_2023,
author = {Pinto, Alessandro and Corso, Anthony and Schmerling, Edward},
publisher = {IEEE},
title = {Leveraging {Compositional} {Methods} for {Modeling} and
{Verification} of an {Autonomous} {Taxi} {System}},
booktitle = {2023 IEEE International Conference on Assured Autonomy
(ICAA)},
pages = {34-43},
date = {2023}
}
Paper
2023
Analysis and Design of Uncertain Cyber-Physical Systems
Alessandro Pinto
Computation-Aware Algorithmic Design for Cyber-Physical SystemsBook chapter
Abstract
Several sources of uncertainty have to be taken into account in the analysis and design of CPS. The set of parameters used in the model of the physical plant of a CPS may be uncertain due, for example, to manufacturing processes that are precise up to some bounded tolerance. Physical quantities are sensed by electronic components that add noise to the sensed signals. Abstraction of the physical world, which is often necessary to limit the complexity of the models used in analysis and at run-time in decision-making, leads to non-determinism. The cyber side of a CPS, which includes both hardware and software components, exposes several types of uncertainty such as failures, latency, and implementation errors. Design processes and tools allow engineers to minimize the impact of these types of uncertainty, and to deliver systems which can be operated with an acceptable level of risk. Control applications tend to have a stable computational workload as filtering, estimation, and control are implemented by software tasks running the same computation independently of data. Real-time operating systems, can provide hard guarantees on the execution of control functions, and several methods can be used to ensure the worst-case execution time of software. Similarly, time-triggered or priorities-based communication protocols can provide hard bounds on the delay experienced by messages exchanged over a network. Failures can be handled through redundant architectures as is typical in safety critical systems. Finally, protection from cyber-attacks can be achieved through physical isolation, careful control of the supply-chain, and other strategies such as authentication and encryption at the boundary of the system. Furthermore, many cyber-physical systems are employed in the automation of processes for which sound models are available. These models have enabled formal analysis and synthesis which further reduce human errors. In the past several years, cyber-physical systems have evolved, primarily due to pervasive connectivity, miniaturization, cost-effectiveness of hardware, and advances in the area of Artificial Intelligence. The complexity of the cyber side of the CPS is constantly increasing as more functionality is moved to software. Correspondingly, the hardware platforms on which the software runs have become more complex. Another evolution has occurred in the area of communications at all levels of the protocol stack allowing disparate computing platforms to be interconnected. Connectivity is pervasive today leveraging technologies such as WiFi, 4G and 5G, and higher-level protocols for the internet of things such as the Message Queuing Telemetry Transport (MQTT). The ability to connect sensing and actuation nodes to the internet enables deployment over a cloud computing infrastructure where data can be aggregated, and computationally expensive algorithms can be executed with virtually unlimited resources. This trend has driven the development of new applications that control societal-scale systems such as the electric grid, transportation, and logistics. Coupling between the physical world and the cyber world can also occur in unconventional ways such as through social media platforms that shape consumer preferences and even opinions of people, driving their physical acts. These new class of applications features an environment which is much more complex to model than traditional physical systems due not only to their scale, but also to new sources and types of uncertainty. Consider, for example, the typical case of echo chambers which is attributed to the effect that machine learning algorithms have on the bias of people. Such behavior is not easily predictable because of high uncertainty in the environment (people), which is only approximately represented by machine learning models, but that is inherently due to lack of knowledge. New models and analysis methods are therefore needed to capture different types of uncertainties, and to analyze these new classes of systems. In this chapter, we start by discussing how cyber-physical systems have evolved from simple controllers to networks of highly autonomous systems. In Section 2, we describe some of the most common sources of uncertainty induced by the platform supporting the software of a CPS, and in Section 3 we review the engineering methods used for analysis and implementation, aiming at reducing the risks due to uncertainty. These two sections show the complexity of dealing with many sources of uncertainty, and how current practice makes use of several models tailored to the analysis of specific classes of uncertainty. In Section 4 we discuss the need for more autonomous systems, the new challenges that they bring in terms of analysis and implementation, and the need for new methods and tools to reason compositionally about aleatoric and epistemic uncertainty. Finally, in Section 5 we present a design methodology and a modeling paradigm that addresses these gaps.
BibTeX
@inbook{pinto_analysis_2023,
author = {Pinto, Alessandro},
publisher = {Springer},
title = {Analysis and {Design} of {Uncertain} {Cyber-Physical}
{Systems}},
booktitle = {Computation-Aware Algorithmic Design for Cyber-Physical
Systems},
pages = {25-53},
date = {2023}
}
Paper
2022
Hierarchical Contract-Based Synthesis for Assurance Cases
Timothy E Wang, Zamira Daw, Pierluigi Nuzzo, Alessandro Pinto
NASA Formal Methods SymposiumConference paper
Abstract
An automatic synthesis problem is often characterized by an overall goal or specification to be satisfied, the set of all possible outcomes, called the design space, and an algorithm for the automatic selection of one or more members from the design space that are provably guaranteed to satisfy the overall specification. A key challenge in automatic synthesis is the complexity of the design space. In this paper, we introduce a formal model, termed hierarchical contract nets, and a framework for the efficient automatic synthesis of hierarchical contract nets, based on a library of refinement relations between contracts and contract nets. We show, via the application of automatic synthesis of assurances cases, that hierarchical contract-based synthesis can mitigate the design space complexity problem. We also show that the approach can bring both the benefits of automating the creation of assurance cases and ensuring that the knowledge from the argumentation experts is captured and reflected in the synthesized assurance cases.
BibTeX
@inproceedings{wang_hierarchical_2022,
author = {Wang, Timothy E and Daw, Zamira and Nuzzo, Pierluigi and
Pinto, Alessandro},
publisher = {Springer},
title = {Hierarchical {Contract-Based} {Synthesis} for {Assurance}
{Cases}},
booktitle = {NASA Formal Methods Symposium},
pages = {175-192},
date = {2022}
}
Paper
2022
Modeling methodology for autonomous cyber-physical systems
Alessandro Pinto
2022 2nd international workshop on computation-aware algorithmic design for cyber-physical systems (CAADCPS)Conference paper
BibTeX
@inproceedings{pinto2022modeling,
author = {Pinto, Alessandro},
publisher = {IEEE},
title = {Modeling Methodology for Autonomous Cyber-Physical Systems},
booktitle = {2022 2nd international workshop on computation-aware
algorithmic design for cyber-physical systems (CAADCPS)},
pages = {1-2},
date = {2022}
}
2021
Requirement Specification, Analysis and Verification for Autonomous Systems
Alessandro Pinto
2021 58th ACM/IEEE Design Automation Conference (DAC)Conference paper
Abstract
The environments and the goals that an autonomous system needs to be able to understand and act upon are not fully known and clearly identifiable at design time, especially for those systems that interact with the physical world. Still, for applications that require a certain level of assurance, requirements, which include the definition of how a system is supposed to interact with its context, need to be defined, analyzed, refined towards an implementation that can be shown to deliver certain guarantees. We first broadly discuss the importance of the early stages of the design process where requirements are defined, and we then discuss the formalisms needed to capture requirements and refine them towards implementation for autonomous systems.
BibTeX
@inproceedings{pinto_requirement_2021,
author = {Pinto, Alessandro},
publisher = {IEEE},
title = {Requirement {Specification,} {Analysis} and {Verification}
for {Autonomous} {Systems}},
booktitle = {2021 58th ACM/IEEE Design Automation Conference (DAC)},
pages = {1315-1318},
date = {2021}
}
Paper
2021
Automated Construction of Knowledge-Bases for Safety Critical Applications: Challenges and Opportunities.
Amit Bhatia, Alessandro Pinto
AAAI Spring Symposium: Combining Machine Learning with Knowledge EngineeringConference paper
Abstract
Creation of machine-usable, high-quality knowledge-bases is a critical prerequisite for many important ap- plications that rely on availability of high-level of autonomous decision-making and reasoning capabilities. Manual construction of knowledge-bases for complex applications is a time-consuming and expensive process. In such application domains, however, a vast amount of knowledge is available in human-readable format, and it could be leveraged to build knowledge-bases automatically. Natural Language Processing (NLP)-based techniques provide an attractive option for this process. The field of NLP has made rapid strides in last sev- eral years and resulted in increased usage across a variety of consumer-facing applications. However, their usage for knowledge-base construction in the aviation industry remains rather limited to date. We present our assessment of using various NLP-based tools for the creation of aviation-focused, high-quality, machine- processable, and human-legible knowledge bases (KBs) for various applications. We identify several gaps, both at the application and fundamental levels, and also identify potential directions for future research that could help overcome the challenges.
BibTeX
@inproceedings{bhatia_automated_2021,
author = {Bhatia, Amit and Pinto, Alessandro},
title = {Automated {Construction} of {Knowledge-Bases} for {Safety}
{Critical} {Applications:} {Challenges} and {Opportunities.}},
booktitle = {AAAI Spring Symposium: Combining Machine Learning with
Knowledge Engineering},
date = {2021}
}
Paper
2019
An open and modular architecture for autonomous and intelligent systems
Alessandro Pinto
2019 IEEE International Conference on Embedded Software and Systems (ICESS)Conference paper
Abstract
Over the past few decades, remarkable progress has been made in the the field of Artificial Intelligence (AI). For some tasks such as games, natural language processing, and image classification, AI powered applications can match or surpass human performance. Despite this progress, truly Autonomous and Intelligent Systems (AIS) serving the needs of, and sharing the environment with humans, are yet to become a commercial reality. AIS engineering requires considerable integration efforts that must be disciplined and guided by a reference model enabling reuse and concurrent design: an open and modular architecture. While several specialized architectures have been developed over the course of few decades, there is a need for a unified approach that supports multi-agency, learning, knowledge representation, reasoning, planning, and run-time verification. In this paper, we propose an open and modular architecture for autonomous and intelligent systems. We start by defining the three primary modules of the architecture, namely situational assessment, knowledge repository and management, and decision making. We then refine each module into functional units and we describe possible interaction patterns among them.
BibTeX
@inproceedings{pinto_open_2019,
author = {Pinto, Alessandro},
publisher = {IEEE},
title = {An Open and Modular Architecture for Autonomous and
Intelligent Systems},
booktitle = {2019 IEEE International Conference on Embedded Software
and Systems (ICESS)},
pages = {1-8},
date = {2019}
}
Paper
2019
Explaining AI decisions using efficient methods for learning sparse Boolean formulae
Susmit Jha, Tuhin Sahai, Vasumathi Raman, Alessandro Pinto, Michael Francis
Journal of Automated ReasoningJournal article
Abstract
In this paper, we consider the problem of learning Boolean formulae from examples obtained by actively querying an oracle that can label these examples as either positive or negative. This problem has received attention in both machine learning as well as formal methods communities, and it has been shown to have exponential worst-case complexity in the general case as well as for many restrictions. In this paper, we focus on learning sparse Boolean formulae which depend on only a small (but unknown) subset of the overall vocabulary of atomic propositions. We propose two algorithms—first, based on binary search in the Hamming space, and the second, based on random walk on the Boolean hypercube, to learn these sparse Boolean formulae with a given confidence. This assumption of sparsity is motivated by the problem of mining explanations for decisions made by artificially intelligent (AI) algorithms, where the explanation of individual decisions may depend on a small but unknown subset of all the inputs to the algorithm. We demonstrate the use of these algorithms in automatically generating explanations of these decisions. These explanations will make intelligent systems more understandable and accountable to human users, facilitate easier audits and provide diagnostic information in the case of failure. The proposed approach treats the AI algorithm as a black-box oracle; hence, it is broadly applicable and agnostic to the specific AI algorithm. We show that the number of examples needed for both proposed algorithms only grows logarithmically with the size of the vocabulary of atomic propositions. We illustrate the practical effectiveness of our approach on a diverse set of case studies.
BibTeX
@article{jha_explaining_2019,
author = {Jha, Susmit and Sahai, Tuhin and Raman, Vasumathi and Pinto,
Alessandro and Francis, Michael},
publisher = {Springer},
title = {Explaining {AI} Decisions Using Efficient Methods for
Learning Sparse {Boolean} Formulae},
journal = {Journal of Automated Reasoning},
volume = {63},
number = {4},
pages = {1055-1075},
date = {2019}
}
Paper
2018
Platform-based design and frameworks: METROPOLIS andMETRO II
Felice Balarin, Massimiliano D’Angelo, Abhijit Davare, Douglas Densmore, Trevor Meyerowitz, Roberto Passerone, Alessandro Pinto, others
Model-based design for embedded systemsBook chapter
BibTeX
@inbook{balarin2018platform,
author = {Balarin, Felice and D’Angelo, Massimiliano and Davare,
Abhijit and Densmore, Douglas and Meyerowitz, Trevor and Passerone,
Roberto and Pinto, Alessandro and {others}},
publisher = {CRC Press},
title = {Platform-Based Design and Frameworks: {METROPOLIS} {andMETRO}
{II}},
booktitle = {Model-based design for embedded systems},
pages = {283-346},
date = {2018}
}
2017
On learning sparse Boolean formulae for explaining AI decisions
Susmit Jha, Vasumathi Raman, Alessandro Pinto, Tuhin Sahai, Michael Francis
NASA Formal Methods SymposiumConference paper
Abstract
In this paper, we consider the problem of learning Boolean formulae from examples obtained by actively querying an oracle that can label these examples as either positive or negative. This problem has received attention in both machine learning as well as formal methods communities, and it has been shown to have exponential worst-case complexity in the general case as well as for many restrictions. In this paper, we focus on learning sparse Boolean formulae which depend on only a small (but unknown) subset of the overall vocabulary of atomic propositions. We propose an efficient algorithm to learn these sparse Boolean formulae with a given confidence. This assumption of sparsity is motivated by the problem of mining explanations for decisions made by artificially intelligent (AI) algorithms, where the explanation of individual decisions may depend on a small but unknown subset of all the inputs to the algorithm. We demonstrate the use of our algorithm in automatically generating explanations of these decisions. These explanations will make intelligent systems more understandable and accountable to human users, facilitate easier audits and provide diagnostic information in the case of failure. The proposed approach treats the AI algorithm as a black-box oracle; hence, it is broadly applicable and agnostic to the specific AI algorithm. We illustrate the practical effectiveness of our approach on a diverse set of case studies.
BibTeX
@inproceedings{jha_learning_2017,
author = {Jha, Susmit and Raman, Vasumathi and Pinto, Alessandro and
Sahai, Tuhin and Francis, Michael},
publisher = {Springer},
title = {On Learning Sparse {Boolean} Formulae for Explaining {AI}
Decisions},
booktitle = {NASA Formal Methods Symposium},
pages = {99-114},
date = {2017}
}
Paper
2017
CSL4P: A contract specification language for platforms
Alessandro Pinto, Alberto L Sangiovanni Vincentelli
Systems EngineeringJournal article
Abstract
The contract-based design formalism supports compositional design and verification, and generalizes many other languages where components are defined in terms of their assumptions and guarantees. Most languages and tools for contract-based design provide constructs to define, instantiate, and connect contracts, but fall short in capturing families of potential architectures in a flexible way. This article presents a Contract-Based Specification Language for Platforms (CSL4P). A platform comprises a set of contract types and a set of constraints called rules. Contract types can be instantiated and connected to form platform instances. While the meaning of composition is predefined in most languages, composition rules are used in CSL4P to provide a finer control on the semantics of interconnections. In addition, the separation of contract types from rules allows users of CSL4P to define different platforms out of the same set of components. This article describes syntax and semantics of the language, a development environment, which includes a compiler and a verification back-end, and an application example.
BibTeX
@article{pinto_csl4p_2017,
author = {Pinto, Alessandro and Sangiovanni Vincentelli, Alberto L},
publisher = {Wiley Online Library},
title = {CSL4P: {A} Contract Specification Language for Platforms},
journal = {Systems Engineering},
volume = {20},
number = {3},
pages = {220-234},
date = {2017}
}
Paper
2015
Metaphysics of planning domain descriptions
Siddharth Srivastava, Stuart Russell, Alessandro Pinto
2015 AAAI Fall Symposium SeriesConference paper
Abstract
Domain models for sequential decision-making typically represent abstract versions of real-world systems. In practice, such abstract representations are compact, easy to maintain, and afford faster solution times. Unfortunately, as we show in the paper, simple ways of abstracting solvable real-world problems may lead to models whose solutions are incorrect with respect to the real-world problem. There is some evidence that such limitations have restricted the applicability of sequential decision-making technology in the real world, as is apparent in the case of task and motion planning in robotics. We show that the situation can be ameliorated by a combination of increased expressive power—for example, allowing angelic nondeterminism in action effects—and new kinds of algorithmic approaches designed to produce correct solutions from initially incorrect or non-Markovian abstract models.
BibTeX
@inproceedings{srivastava_metaphysics_2015,
author = {Srivastava, Siddharth and Russell, Stuart and Pinto,
Alessandro},
title = {Metaphysics of Planning Domain Descriptions},
booktitle = {2015 AAAI Fall Symposium Series},
date = {2015}
}
Paper
2014
Hierarchical multi-objective planning: From mission specifications to contingency management
Xuchu Dennis Ding, Brendan Englot, Alessandro Pinto, Alberto Speranzon, Amit Surana
2014 IEEE international conference on robotics and automation (ICRA)Conference paper
Abstract
We propose a hierarchical planning framework for mission planning and execution in uncertain and dynamic environments. We consider missions that involve motion planning in large, cluttered environments, trading off mission objectives while satisfying logical/spatial/temporal constraints. Our framework enables the decomposition of the planning problem across different layers, leveraging the difference in spatial and temporal scales of the mission objectives. We show that this framework facilitates contingency management under unanticipated events. Interaction between the various layers requires consistent model abstractions and common message semantics. To satisfy these requirements, we adopt a generic knowledge-based architecture that is independent from a specific application domain. We show a specific instance of our framework using a Constrained Markov Decision Process (CMDP) planner at the higher level and a Multi-Objective Probabilistic Roadmap (MO-PRM) planner at the lower level. The resulting planning system is tested in a realistic scenario where an agent is tasked with a mission in a large urban threat rich environment under dynamic uncertain conditions. The mission specification includes a Linear Temporal Logic (LTL) formula that defines the desired behaviors, a list of metrics to be optimized and a list of constraints on time, resources and probability of mission success.
BibTeX
@inproceedings{ding_hierarchical_2014,
author = {Ding, Xuchu Dennis and Englot, Brendan and Pinto, Alessandro
and Speranzon, Alberto and Surana, Amit},
publisher = {IEEE},
title = {Hierarchical Multi-Objective Planning: {From} Mission
Specifications to Contingency Management},
booktitle = {2014 IEEE international conference on robotics and
automation (ICRA)},
pages = {3735-3742},
date = {2014}
}
Paper
2014
Computing Probability Distributions over a Hybrid State Space: Case Study and Practical Limitations
Alessandro Pinto, George A Mathew
Conference paper
BibTeX
@inproceedings{pinto_computing_2014,
author = {Pinto, Alessandro and Mathew, George A},
title = {Computing {Probability} {Distributions} over a {Hybrid}
{State} {Space:} {Case} {Study} and {Practical} {Limitations}},
date = {2014}
}
2013
A complexity metric for concurrent finite state machine based embedded software
Liangpeng Guo, Alberto Sangiovanni Vincentelli, Alessandro Pinto
2013 8th IEEE International Symposium on Industrial Embedded Systems (SIES)Conference paper
Abstract
The development cost of safety-critical embedded systems is dominated today by the cost of software including verification and validation. This cost is typically related to the complexity of the software functions implementing the desired system behavior in nominal and off-nominal conditions. A widely used measure of complexity is the cyclomatic number, which is computed on the implementation code. However this technique is not effective when model-based development and code generation are used because the complexity of the software also depends on the communication and execution semantics of the models. This paper proposes a model-based complexity number that is defined on the decision diagram (DD) representation of the system functionality. The proposed complexity number gives an upper bound on the number of tests that are necessary to achieve Condition/Decision (C/D) coverage (which is required for safety critical systems). We show that the number of tests is related to the min-flow/max-cut computed on the DD. By comparing the proposed metric with the cyclomatic complexity, we show that the former seems to be better suited for capturing the complexity of the model than the latter. A case study on an aircraft power system shows that the complexity metric has applications in functional partitioning and architecture selection.
BibTeX
@inproceedings{guo_complexity_2013,
author = {Guo, Liangpeng and Vincentelli, Alberto Sangiovanni and
Pinto, Alessandro},
publisher = {IEEE},
title = {A Complexity Metric for Concurrent Finite State Machine Based
Embedded Software},
booktitle = {2013 8th IEEE International Symposium on Industrial
Embedded Systems (SIES)},
pages = {189-195},
date = {2013}
}
Paper
2013
Strategic planning under uncertainties via constrained Markov decision processes
Xu Chu Ding, Alessandro Pinto, Amit Surana
2013 IEEE International Conference on Robotics and AutomationConference paper
Abstract
In this paper, we propose a hierarchical mission planner where the state of the world and of the mission are abstracted into corresponding states of a Markov Decision Process (MDP). Transitions in the MDP represent abstract motion actions that are planned by a lower level probabilistic planner. The cost structure of the MDP is multi-dimensional: each state-action pair is annotated with a vector of metrics such as time and resource requirements. A mission specification is divided into three parts: a temporal logic formula defined over state propositions, the choice of the primary cost, and constraints on the remaining secondary costs. The planning problem is formulated as finding the optimal policy of a Constrained Markov Decision Process with above mission specification. The resulting planning system is tested in a mission where an agent is tasked with a complex mission in a urban hostile environment.
BibTeX
@inproceedings{ding_strategic_2013,
author = {Ding, Xu Chu and Pinto, Alessandro and Surana, Amit},
publisher = {IEEE},
title = {Strategic Planning Under Uncertainties via Constrained
{Markov} Decision Processes},
booktitle = {2013 IEEE International Conference on Robotics and
Automation},
pages = {4568-4575},
date = {2013}
}
Paper
2012
Correct-by-construction and optimal synthesis of beacon-enabled ZigBee network
Songyan Xu, Ratnesh Kumar, Alessandro Pinto
IEEE Transactions on Automation Science and EngineeringJournal article
Abstract
In this paper we develop a formal approach for the synthesis of a cost-effective and correct-by-construction communication network (focusing on ZigBee wireless networks) subject to a set of end-to-end communication constraints of latency, bandwidth and error-rate, together with the constraints of the network protocols and the desired geographical placement of the network. We also develop a software platform to implement the proposed approach for network synthesis, and apply it to a practical wireless network synthesis for centralized as well as distributed estimation application.
BibTeX
@article{xu_correct-by-construction_2012,
author = {Xu, Songyan and Kumar, Ratnesh and Pinto, Alessandro},
publisher = {IEEE},
title = {Correct-by-Construction and Optimal Synthesis of
Beacon-Enabled {ZigBee} Network},
journal = {IEEE Transactions on Automation Science and Engineering},
volume = {10},
number = {1},
pages = {137-144},
date = {2012}
}
Paper
2012
Stringent safety design and verification methods for VTOL unmanned aerial vehicles
I Cherepinsky, A Pinto
Proceedings of the American Helicopter Society 68th Annual Forum, Fort Worth, TXConference paper
BibTeX
@inproceedings{cherepinsky_stringent_2012,
author = {Cherepinsky, I and Pinto, A},
title = {Stringent Safety Design and Verification Methods for {VTOL}
Unmanned Aerial Vehicles},
booktitle = {Proceedings of the American Helicopter Society 68th
Annual Forum, Fort Worth, TX},
date = {2012}
}
2012
Methods and tools to enable the design and verification of intelligent systems
A Pinto
AIAA Infotech at AerospaceJournal article
BibTeX
@article{pinto_methods_2012,
author = {Pinto, A},
title = {Methods and Tools to Enable the Design and Verification of
Intelligent Systems},
journal = {AIAA Infotech at Aerospace},
date = {2012}
}
Paper
2011
Meta II complex systems design and analysis (CODA)
BT Murray, A Pinto, R Skelding, O De Weck, H Zhu, S Nair, N Shougarian, K Sinha, S Bopardikar, L Zeidner
DTIC DocumentJournal article
BibTeX
@article{murray2011meta,
author = {Murray, BT and Pinto, A and Skelding, R and De Weck, O and
Zhu, H and Nair, S and Shougarian, N and Sinha, K and Bopardikar, S
and Zeidner, L},
title = {Meta {II} Complex Systems Design and Analysis {(CODA)}},
journal = {DTIC Document},
date = {2011}
}
2011
Synthesis of distributed execution platforms for cyber-physical systems with applications to high-performance buildings
Francesco Leonardi, Alessandro Pinto, Luca P Carloni
2011 IEEE/ACM Second International Conference on Cyber-Physical SystemsConference paper
Abstract
We propose a methodology, and its embodiment into a design flow, to realize execution platforms for high-performance building applications. This is an example of a class of cyberphysical systems where a network of sensors, controllers, and actuators must be designed under physical spatial constraints to implement various types of signal processing and control tasks. In our approach, the applications are specified using the dataflow model of computation while the building dictates the physical constraints, including the position of sensors and actuators. We present a rigorous formulation of the design-space exploration problem and we propose to solve it by progressing through a sequence of refinement steps from specification to detailed implementation. Two key steps are the synthesis of the computation platform and the synthesis of the communication network. Combined, they allow us to automatically derive an optimal implementation through the selection and composition of processing and networking elements from given technology libraries. We demonstrate the applicability of our approach by comparing it to the manual design of a given case study: the real-time estimation of building occupancy using a network of video cameras.
BibTeX
@inproceedings{leonardi_synthesis_2011,
author = {Leonardi, Francesco and Pinto, Alessandro and Carloni, Luca
P},
publisher = {IEEE},
title = {Synthesis of Distributed Execution Platforms for
Cyber-Physical Systems with Applications to High-Performance
Buildings},
booktitle = {2011 IEEE/ACM Second International Conference on
Cyber-Physical Systems},
pages = {215-224},
date = {2011}
}
Paper
2011
Stochastic analysis and design of systems
George A Mathew, Alessandro Pinto
UNITED TECHNOLOGIES CORP HARTFORD CTTechnical report
Abstract
Analysis and design methods for stochastic hybrid dynamical systems are presented. Analysis methods include reachability analysis as well as statistical approaches. System refinement and decomposition are explored as possible approaches to deal with complexity. Findings show that analysis of this class of systems is not scalable. A promising approach is demonstrated which relies on the automatic construction of decentralized control systems using desirable properties as constraints. The synthesized system does not require to be analyzed thereby cutting the analysis effort. This approach is promising but for now limited in its use.
BibTeX
@report{mathew_stochastic_2011,
author = {Mathew, George A and Pinto, Alessandro},
publisher = {UNITED TECHNOLOGIES CORP HARTFORD CT},
title = {Stochastic Analysis and Design of Systems},
date = {2011}
}
Paper
2011
Scalable approach to uncertainty quantification and robust design of interconnected dynamical systems
Andrzej Banaszuk, Vladimir A Fonoberov, Thomas A Frewen, Marin Kobilarov, George Mathew, Igor Mezic, Alessandro Pinto, Tuhin Sahai, Harshad Sane, Alberto Speranzon, others
Annual Reviews in ControlJournal article
Abstract
Development of robust dynamical systems and networks such as autonomous aircraft systems capable of accomplishing complex missions faces challenges due to the dynamically evolving uncertainties coming from model uncertainties, necessity to operate in a hostile cluttered urban environment, and the distributed and dynamic nature of the communication and computation resources. Model-based robust design is difficult because of the complexity of the hybrid dynamic models including continuous vehicle dynamics, the discrete models of computations and communications, and the size of the problem. We will overview recent advances in methodology and tools to model, analyze, and design robust autonomous aerospace systems operating in uncertain environment, with stress on efficient uncertainty quantification and robust design using the case studies of the mission including model-based target tracking and search, and trajectory planning in uncertain urban environment. To show that the methodology is generally applicable to uncertain dynamical systems, we will also show examples of application of the new methods to efficient uncertainty quantification of energy usage in buildings, and stability assessment of interconnected power networks.
BibTeX
@article{banaszuk_scalable_2011,
author = {Banaszuk, Andrzej and Fonoberov, Vladimir A and Frewen,
Thomas A and Kobilarov, Marin and Mathew, George and Mezic, Igor and
Pinto, Alessandro and Sahai, Tuhin and Sane, Harshad and Speranzon,
Alberto and {others}},
publisher = {Elsevier},
title = {Scalable Approach to Uncertainty Quantification and Robust
Design of Interconnected Dynamical Systems},
journal = {Annual Reviews in Control},
volume = {35},
number = {1},
pages = {77-98},
date = {2011}
}
Paper
2011
Probabilistically safe vehicle control in a hostile environment
Igor Cizelj, Xu Chu Dennis Ding, Morteza Lahijanian, Alessandro Pinto, Calin Belta
IFAC Proceedings VolumesJournal article
Abstract
In this paper we present an approach to control a vehicle in a hostile environment with static obstacles and moving adversaries. The vehicle is required to satisfy a mission objective expressed as a temporal logic specification over a set of properties satisfied at regions of a partitioned environment. We model the movements of adversaries in between regions of the environment as Poisson processes. Furthermore, we assume that the time it takes for the vehicle to traverse in between two facets of a region is exponentially distributed, and we obtain the rate of this exponential distribution from a simulator of the environment. We capture the motion of the vehicle and the vehicle updates of adversaries distributions as a Markov Decision Process. Using tools in Probabilistic Computational Tree Logic, we find a control strategy for the vehicle that maximizes the probability of accomplishing the mission objective. We demonstrate our approach with illustrative case studies.
BibTeX
@article{cizelj_probabilistically_2011,
author = {Cizelj, Igor and Ding, Xu Chu Dennis and Lahijanian, Morteza
and Pinto, Alessandro and Belta, Calin},
publisher = {Elsevier},
title = {Probabilistically Safe Vehicle Control in a Hostile
Environment},
journal = {IFAC Proceedings Volumes},
volume = {44},
number = {1},
pages = {11803-11808},
date = {2011}
}
Paper
2011
Model-based hierarchical optimal control design for HVAC systems
Mehdi Maasoumy, Alessandro Pinto, Alberto Sangiovanni-Vincentelli
Dynamic Systems and Control ConferenceConference paper
Abstract
A hierarchical control architecture for balancing comfort and energy consumption in buildings is presented. The control design is based on a simplified, yet accurate model of the temperature within each room of the building. The model is validated against real measurements. The control architecture comprises a first level that regulates low level quantities such as air flow, and a second level that balances comfort (i.e. distance between the desired and actual temperature) and energy consumption (i.e. total energy consumed for the required level of comfort). We show the effectiveness of our approach by simulation using validated models.
BibTeX
@inproceedings{maasoumy_model-based_2011,
author = {Maasoumy, Mehdi and Pinto, Alessandro and
Sangiovanni-Vincentelli, Alberto},
title = {Model-Based Hierarchical Optimal Control Design for {HVAC}
Systems},
booktitle = {Dynamic Systems and Control Conference},
volume = {54754},
pages = {271-278},
date = {2011}
}
Paper
2011
A hierarchical wireless network architecture for building automation and control systems
M Mozumdar, Alberto Puggelli, Alessandro Pinto, Luciano Lavagno, Alberto L Sangiovanni-Vincentelli
Proceedings of the 7th International Conference on Networking and Services (ICNS)Conference paper
Abstract
The building automation industry is experiencing a sudden increase in the complexity of control systems, mainly due to the push towards energy efficient buildings. These systems are necessarily distributed and rely on a communication network to gather data from sensors, produce intermediate results, and send commands to actuators. These networks should be cost effective, and should be flexible enough to be easily reconfigured if the building usage changes over the years. Wireless sensor and actuator networks are, therefore, key enablers. In this paper, we propose a hierarchical wireless network architecture for building automation and control systems and a protocol to manage it. We implement gradient based routing (for collecting data) and label switching table (for disseminating configuration commands), thereby supporting upstream and downstream data flows across the network.
BibTeX
@inproceedings{mozumdar_hierarchical_2011,
author = {Mozumdar, M and Puggelli, Alberto and Pinto, Alessandro and
Lavagno, Luciano and Sangiovanni-Vincentelli, Alberto L},
title = {A Hierarchical Wireless Network Architecture for Building
Automation and Control Systems},
booktitle = {Proceedings of the 7th International Conference on
Networking and Services (ICNS)},
date = {2011}
}
Paper
2011
Optimal design of a class of hybrid systems with uncertain parameters
George Mathew, Alessandro Pinto
2011 50th IEEE Conference on Decision and Control and European Control ConferenceConference paper
Abstract
Many modern engineering systems can be mathematically modeled as hybrid systems. For many such systems, there may be uncertain parameters and also parameters that can be adjusted so that the system achieves some optimal performance. It is important to develop efficient numerical tools and software to optimize for these adjustable parameters. We focus on a specific class of hybrid systems where mode transitions are dependent only on the amount of time spent in a mode (or equivalently a clock value). The amount of time spent in each mode is assumed to be a random variable with a known distribution. We aim to design or choose values for the free parameters in each mode of the hybrid system so that the expected value of some meaningful cost-function is minimized. This can be framed as a stochastic optimization problem. We use the sample average approximation method to solve the resulting stochastic optimization problem. We illustrate the method for the optimal design of a thermal management system of a prototypical aircraft.
BibTeX
@inproceedings{mathew_optimal_2011,
author = {Mathew, George and Pinto, Alessandro},
publisher = {IEEE},
title = {Optimal Design of a Class of Hybrid Systems with Uncertain
Parameters},
booktitle = {2011 50th IEEE Conference on Decision and Control and
European Control Conference},
pages = {539-544},
date = {2011}
}
Paper
2010
A model-based end-to-end toolchain for the probabilistic analysis of complex systems
Alessandro Pinto, Sudha Krishnamurthy, Suresh Kannan
2010 IEEE International Conference on Automation Science and EngineeringConference paper
Abstract
We present a model-based environment for the probabilistic analysis of systems operating under uncertain conditions. This uncertainty may result from either the environments in which they operate or the platforms on which they execute. Available probabilistic analysis methods require to capture the system specification using languages that are semantically very close to Markov Chains. However, designers use model-based environments working at much higher abstraction levels. We present an integrated tool, called StoNES (Stochastic analysis of Networked Embedded Systems), that automates the model transformation and probabilistic analysis of systems. We apply our translation and analysis methodology to explore the trade-off between sensor accuracy and computational speed for the vision algorithm of an autonomous helicopter system.
BibTeX
@inproceedings{pinto_model-based_2010,
author = {Pinto, Alessandro and Krishnamurthy, Sudha and Kannan,
Suresh},
publisher = {IEEE},
title = {A Model-Based End-to-End Toolchain for the Probabilistic
Analysis of Complex Systems},
booktitle = {2010 IEEE International Conference on Automation Science
and Engineering},
pages = {994-1000},
date = {2010}
}
Paper
2010
A design flow for building automation and control systems
Yang Yang, Alessandro Pinto, Alberto Sangiovanni-Vincentelli, Qi Zhu
2010 31st IEEE Real-Time Systems SymposiumConference paper
Abstract
We propose a system-level design flow for building automation and control (BAC) systems. The input to the design flow is a high level description of the control algorithms given in a model-based environment such as Simulink. The input specification is translated into an intermediate format, and then automatically refined into a distributed implementation. Refinement includes optimal mapping of the functional specification on a set of computation and communication resources, and software synthesis, which generates code for each component in the mapped design while guaranteeing semantic equivalence with the original specification. Experiments with a temperature control system are presented to illustrate the flow
BibTeX
@inproceedings{yang_design_2010,
author = {Yang, Yang and Pinto, Alessandro and
Sangiovanni-Vincentelli, Alberto and Zhu, Qi},
publisher = {IEEE},
title = {A Design Flow for Building Automation and Control Systems},
booktitle = {2010 31st IEEE Real-Time Systems Symposium},
pages = {105-116},
date = {2010}
}
Paper
2010
Markov modeling of stochastic hybrid systems
George Mathew, Alessandro Pinto
2010 48th Annual Allerton Conference on Communication, Control, and Computing (Allerton)Conference paper
Abstract
Hybrid systems are a useful abstraction for systems that have a combination of discrete and continuous dynamics. For typical examples of hybrid systems, there can be various sources of stochasticity. The source of stochasticity can be in the dynamics of the continuous states, the probabilistic switching between various modes of the system and the probabilistic resetting of the continuous state after switches. Such systems can be mathematically modeled by Discrete Time Stochastic Hybrid Systems (DTSHS). If the uncertainty in the initial condition of the stochastic hybrid system is specified by a probability distribution, it is useful to compute the probability distribution of the state of the system for some time in the future. This would allow one to quantify the probability of the system to be in an undesired or unsafe set. Such computations can be useful for probabilistic verification and validation of systems. In this paper, we discuss state space models for DTSHS and present computational methods to propagate probability distributions for DTSHS.
BibTeX
@inproceedings{mathew_markov_2010,
author = {Mathew, George and Pinto, Alessandro},
publisher = {IEEE},
title = {Markov Modeling of Stochastic Hybrid Systems},
booktitle = {2010 48th Annual Allerton Conference on Communication,
Control, and Computing (Allerton)},
pages = {1707-1713},
date = {2010}
}
Paper
2010
Developing design tools for uncertain systems in an industrial setting
Alessandro Pinto, Sudha Krishnamurthy
2010 48th Annual Allerton Conference on Communication, Control, and Computing (Allerton)Conference paper
Abstract
We motivate the need for a cyber-physical system analysis and design tool that embraces uncertainty as key characteristic of these type of systems. We outline the features that such tool should provide and we present a prototype implementation. The challenges faced during its development go beyond the sheer complexity of analyzing large Markov Models. We close the paper with some examples of analysis of uncertain systems.
BibTeX
@inproceedings{pinto_developing_2010,
author = {Pinto, Alessandro and Krishnamurthy, Sudha},
publisher = {IEEE},
title = {Developing Design Tools for Uncertain Systems in an
Industrial Setting},
booktitle = {2010 48th Annual Allerton Conference on Communication,
Control, and Computing (Allerton)},
pages = {1714-1721},
date = {2010}
}
Paper
2010
Design system for managing complexity in aerospace systems
Sandor Becz, Alessandro Pinto, Lawrence Zeidner, Ritest Khire, Hayden Reeve, Andrzej Banaszuk
10th AIAA Aviation Technology, Integration, and Operations (ATIO) ConferenceConference paper
Abstract
A new generation of aerospace systems has introduced more-electric technologies and highly coupled architectures, leading to a substantial increase in design complexity. The inability of current design systems to manage this complexity has lead to substantial cost and schedule overruns during the development of new military and commercial platforms. This paper presents the framework for a new design process to manage system complexity and highlights four key elements: 1) Abstraction-based design tools to allow complex interactions to be assessed at a high level of abstraction early in the design cycle; 2) Quantitative complexity metrics that can guide early design decisions and identify sources of complexity within candidate designs; 3) Advanced architecture synthesis methods that enable the formal and automated architecture synthesis, enumeration, and evaluation of feasible architecture options; and 4) Robust uncertainty management for identifying strong coupling between systems with high uncertainty, thereby allowing the identification and management of key risks.
BibTeX
@inproceedings{becz_design_2010,
author = {Becz, Sandor and Pinto, Alessandro and Zeidner, Lawrence and
Khire, Ritest and Reeve, Hayden and Banaszuk, Andrzej},
title = {Design System for Managing Complexity in Aerospace Systems},
booktitle = {10th AIAA Aviation Technology, Integration, and
Operations (ATIO) Conference},
pages = {9223},
date = {2010}
}
Paper
2010
Correct-by-construction design of aircraft electric power systems
Alessandro Pinto, Sandor Becz, Hayden Reeve
10th AIAA Aviation Technology, Integration, and Operations (ATIO) ConferenceConference paper
Abstract
We provide an optimization oriented formalization of correct-by-construction design following the principles of Platform-Based Design.1 The design proceeds by refinement steps. At each step, a specification is given in terms of requirements to be satisfied by an implementation. The implementation choices are implicitly captured by a set of components, their properties, and their composition rules. A class of candidate implementations of the specification is derived by formulating and solving an optimization problem. The implementation becomes the specification for the next step in the design flow. We show how the optimization oriented formalization enables design space exploration, and we present the trade-offs involved in the selection of the refinement steps. We show how the methodology can be applied to the design of electric power systems by decomposing the design flow into the following steps: generator selection, generation of the connection configuration under faults, and topology design of the power distribution system.
BibTeX
@inproceedings{pinto_correct-by-construction_2010,
author = {Pinto, Alessandro and Becz, Sandor and Reeve, Hayden},
title = {Correct-by-Construction Design of Aircraft Electric Power
Systems},
booktitle = {10th AIAA Aviation Technology, Integration, and
Operations (ATIO) Conference},
pages = {9263},
date = {2010}
}
Paper
2010
Analysis of Stochastic Automata Networks using copula functions
Amit Surana, Alessandro Pinto
2010 48th Annual Allerton Conference on Communication, Control, and Computing (Allerton)Conference paper
Abstract
In this paper we develop a copula based approximation framework for scalable analysis of Stochastic Automata Networks (SAN) arising in reliability analysis, and can be described by CTMCs. Copulas provide a general approach to model joint distributions in terms of their marginals. Using copulas functions, the dependencies between the interacting automata in the SAN can be captured in terms of local state probabilities associated with the automata involved, avoiding the need of reachability analysis, which is cursed with state space explosion. We prove results related to invariance of copula with system parameters, and consistency of the approximation. We also outline an empirical procedure for determining copulas that can best represent the underlying dependence in a given SAN. We illustrate this approach through various examples of increasing complexity.
BibTeX
@inproceedings{surana_analysis_2010,
author = {Surana, Amit and Pinto, Alessandro},
publisher = {IEEE},
title = {Analysis of {Stochastic} {Automata} {Networks} Using Copula
Functions},
booktitle = {2010 48th Annual Allerton Conference on Communication,
Control, and Computing (Allerton)},
pages = {1699-1706},
date = {2010}
}
Paper
2009
Accurate predictive interconnect modeling for system-level design
Luca P Carloni, Andrew B Kahng, Swamy V Muddu, Alessandro Pinto, Kambiz Samadi, Puneet Sharma
IEEE transactions on very large scale integration (VLSI) systemsJournal article
Abstract
We propose new accurate predictive models for the delay, power, and area of buffered interconnects to enable a more effective system-level design exploration with existing and future nanometer technology processes. We show that our models are significantly more accurate than previous models - essentially matching sign-off analyses. We integrate our models in the COSI-OCC communication synthesis infrastructure and show how they impact the feasibility and optimality of the network-on-chip architectures that are synthesized by this tool.
BibTeX
@article{carloni_accurate_2009,
author = {Carloni, Luca P and Kahng, Andrew B and Muddu, Swamy V and
Pinto, Alessandro and Samadi, Kambiz and Sharma, Puneet},
publisher = {IEEE},
title = {Accurate Predictive Interconnect Modeling for System-Level
Design},
journal = {IEEE transactions on very large scale integration (VLSI)
systems},
volume = {18},
number = {4},
pages = {679-684},
date = {2009}
}
Paper
2009
Synthesis of wireless time-triggered embedded networks for networked control systems
Alessandro Pinto, Ratnesh Kumar, Songyan Xu
2009 IEEE International Conference on Automation Science and EngineeringConference paper
Abstract
In this paper, we extend our previous work by including the decisions for connection-scheduling as part of the automated synthesis of embedded networks for networked control systems. We propose an automated approach for the synthesis of a cost-effective and correct-by-construction communication network for embedded applications subject to a set of end-to-end communication constraints of latency, bandwidth, and error-rate, the geometry constraints arising due to a desired geographical placement of the network, and a set of scheduling constraints. We also apply the proposed approach for network synthesis with scheduling to the synthesis of wireless networks for centralized and distributed state estimation in building automation and control. The proposed approach is general enough to be applicable to wired and wireless network synthesis.
BibTeX
@inproceedings{pinto_synthesis_2009,
author = {Pinto, Alessandro and Kumar, Ratnesh and Xu, Songyan},
publisher = {IEEE},
title = {Synthesis of Wireless Time-Triggered Embedded Networks for
Networked Control Systems},
booktitle = {2009 IEEE International Conference on Automation Science
and Engineering},
pages = {397-402},
date = {2009}
}
Paper
2009
A case study in distributed deployment of embedded software for camera networks
Francesco Leonardi, Alessandro Pinto, Luca P Carloni
2009 Design, Automation & Test in Europe Conference & ExhibitionConference paper
Abstract
We present an embedded software application for the real-time estimation of building occupancy using a network of video cameras. We analyze a series of alternative decompositions of the main application tasks and profile each of them by running the corresponding embedded software on three different processors. Based on the profiling measures, we build various alternative embedded platforms by combining different embedded processors, memory modules and network interfaces. In particular, we consider the choice of two possible network technologies: ARCnet and Ethernet. After deriving an analytical model of the network costs, we use it to complete an exploration of the design space as we scale the number of video cameras in an hypothetical building. We compare our results with those obtained for two real buildings of different characteristics. We conclude discussing the results of our case study in the broader context of other camera-network applications.
BibTeX
@inproceedings{leonardi_case_2009,
author = {Leonardi, Francesco and Pinto, Alessandro and Carloni, Luca
P},
publisher = {IEEE},
title = {A Case Study in Distributed Deployment of Embedded Software
for Camera Networks},
booktitle = {2009 Design, Automation \& Test in Europe Conference \&
Exhibition},
pages = {1006-1011},
date = {2009}
}
Paper
2009
A methodology for constraint-driven synthesis of on-chip communications
Alessandro Pinto, Luca P Carloni, Alberto L Sangiovanni-Vincentelli
IEEE Transactions on Computer-Aided Design of Integrated Circuits and SystemsJournal article
Abstract
We present a methodology and an optimization framework for the synthesis of on-chip communication through the assembly of components such as interfaces, routers, buses and links, from a target library. Models for functionality, cost, and performance of each element are captured in the library together with their composition rules. We develop a mathematical framework to model communication at different levels of abstraction from the point-to-point input specification to the library elements and the final implementation.
BibTeX
@article{pinto_methodology_2009,
author = {Pinto, Alessandro and Carloni, Luca P and
Sangiovanni-Vincentelli, Alberto L},
publisher = {IEEE},
title = {A Methodology for Constraint-Driven Synthesis of on-Chip
Communications},
journal = {IEEE Transactions on Computer-Aided Design of Integrated
Circuits and Systems},
volume = {28},
number = {3},
pages = {364-377},
date = {2009}
}
Paper
Source
2008
Synthesis of embedded networks for building automation and control
Alessandro Pinto, Massimiliano D’Angelo, Carlo Fischione, Eelco Scholte, Alberto Sangiovanni-Vincentelli
2008 American Control ConferenceConference paper
Abstract
We present a methodology and a software framework for the automatic design exploration of the communication network among sensors, actuators and controllers in building automation systems. Given 1) a set of end-toend latency, throughput and packet error rate constraints between nodes, 2) the building geometry, and 3) a library of communication components together with their performance and cost characterization, a synthesis algorithm produces a network implementation that satisfies all end-to-end constraints and that is optimal with respect to installation and maintenance cost. The methodology is applied to the synthesis of wireless networks for an essential step in any control algorithm in a distributed environment: the estimation of control variables such as temperature and air-flow in buildings.
BibTeX
@inproceedings{pinto_synthesis_2008,
author = {Pinto, Alessandro and D’Angelo, Massimiliano and Fischione,
Carlo and Scholte, Eelco and Sangiovanni-Vincentelli, Alberto},
publisher = {IEEE},
title = {Synthesis of Embedded Networks for Building Automation and
Control},
booktitle = {2008 American Control Conference},
pages = {920-925},
date = {2008}
}
Paper
2008
Outage-based rate maximization in cdma wireless networks
M D’Angelo, Carlo Fischione, Matteo Butussi, Alessandro Pinto, Al Sangiovanni-Vincentelli
IEEE GLOBECOM 2008-2008 IEEE Global Telecommunications ConferenceConference paper
Abstract
The problem of maximizing the sum of the transmit rates while limiting the outage probability below an appropriate threshold is investigated for networks where the nodes have limited processing capabilities. We focus on CDMA wireless network whose rates are characterized under mixed Rayleigh- lognormal fading. The outage probability is given implicitly by a complex function so that solving the optimization problem requires substantial computing. In this paper, we propose a novel explicit approximation of this function that allows solving the problem in an affordable manner. We propose two solutions of the maximization problem with the simplified outage probability constraint: one solves the problem using mixed integer-real programming. The other relaxes the constraints that rates be integers yielding a standard convex programming optimization that can be solved much faster. Numerical results show that our approaches perform well for average values of the outage requirements.
BibTeX
@inproceedings{dangelo_outage-based_2008,
author = {D’Angelo, M and Fischione, Carlo and Butussi, Matteo and
Pinto, Alessandro and Sangiovanni-Vincentelli, Al},
publisher = {IEEE},
title = {Outage-Based Rate Maximization in Cdma Wireless Networks},
booktitle = {IEEE GLOBECOM 2008-2008 IEEE Global Telecommunications
Conference},
pages = {1-6},
date = {2008}
}
Paper
2008
Interconnect modeling for improved system-level design optimization
Luca Carloni, Andrew B Kahng, Swamy Muddu, Alessandro Pinto, Kambiz Samadi, Puneet Sharma
2008 Asia and South Pacific Design Automation ConferenceConference paper
Abstract
Accurate modeling of delay, power, and area of interconnections early in the design phase is crucial for effective system-level optimization. Models presently used in system-level optimizations, such as network-on-chip (NoC) synthesis, are inaccurate in the presence of deep-submicron effects. In this paper, we propose new, highly accurate models for delay and power in buffered interconnects; these models are usable by system-level designers for existing and future technologies. We present a general and transferable methodology to construct our models from a wide variety of reliable sources (Liberty, LEF/ITF, ITRS, PTM, etc.). The modeling infrastructure, and a number of characterized technologies, are available as open source. Our models comprehend key interconnect circuit and layout design styles, and a power-efficient buffering technique that overcomes unrealities of previous delay-driven buffering techniques. We show that our models are significantly more accurate than previous models for global and intermediate buffered interconnects in 90 nm and 65 nm foundry processes - essentially matching signoff analyses. We also integrate our models in the COSI-OCC synthesis tool and show that the more accurate modeling significantly affects optimal/achievable architectures that are synthesized by the tool. The increased accuracy provided by our models enables system-level designers to obtain better assessments of the achievable performance/power/area tradeoffs for (communication-centric aspects of) system design, with negligible setup and overhead burdens.
BibTeX
@inproceedings{carloni_interconnect_2008,
author = {Carloni, Luca and Kahng, Andrew B and Muddu, Swamy and
Pinto, Alessandro and Samadi, Kambiz and Sharma, Puneet},
publisher = {IEEE},
title = {Interconnect Modeling for Improved System-Level Design
Optimization},
booktitle = {2008 Asia and South Pacific Design Automation Conference},
pages = {258-264},
date = {2008}
}
Paper
2008
COSI: A framework for the design of interconnection networks
Alessandro Pinto, Luca P Carloni, Alberto Sangiovanni-Vincentelli
IEEE Design & Test of ComputersJournal article
Abstract
This article presents a software framework for communication infrastructure synthesis of distributed systems, which is critical for overall system performance in communication-based design. Particular emphasis is given to on-chip interconnect synthesis of multicore designs.
BibTeX
@article{pinto_cosi_2008,
author = {Pinto, Alessandro and Carloni, Luca P and
Sangiovanni-Vincentelli, Alberto},
publisher = {IEEE},
title = {COSI: {A} Framework for the Design of Interconnection
Networks},
journal = {IEEE Design \& Test of Computers},
volume = {25},
number = {5},
pages = {402-415},
date = {2008}
}
Paper
2007
A next-generation design framework for platform-based design
Abhijit Davare, Douglas Densmore, Trevor Meyerowitz, Alessandro Pinto, Alberto Sangiovanni-Vincentelli, Guang Yang, Haibo Zeng, Qi Zhu
Conference on using hardware design and verification languages (DVCon)Conference paper
Abstract
The platform-based design methodology [1] is based on the usage of formal modeling techniques, clearly defined abstraction levels and the separation of concerns to enable an effective design process. The METROPOLIS framework embodies the platform-based design methodology and has been applied to a number of case studies across multiple domains. Based on these experiences, we have identified three key features that need to be enhanced: heterogeneous IP import, orthogonalization of performance from behavior, and design space exploration. The next generation METRO II framework incorporates these advanced features. The main concepts underlying METRO II are described in this paper and illustrated with a small example.
BibTeX
@inproceedings{davare_next-generation_2007,
author = {Davare, Abhijit and Densmore, Douglas and Meyerowitz, Trevor
and Pinto, Alessandro and Sangiovanni-Vincentelli, Alberto and Yang,
Guang and Zeng, Haibo and Zhu, Qi},
title = {A Next-Generation Design Framework for Platform-Based Design},
booktitle = {Conference on using hardware design and verification
languages (DVCon)},
volume = {152},
date = {2007}
}
Paper
2007
A communication synthesis infrastructure for heterogeneous networked control systems and its application to building automation and control
Alessandro Pinto, Luca P Carloni, Alberto L Sangiovanni-Vincentelli
Proceedings of the 7th ACM & IEEE international conference on Embedded softwareConference paper
Abstract
In networked control systems the controller of a physicallydistributed plant is implemented as a collection of tightlyinteracting, concurrent processes running on a distributed execution platform. The execution platform consists of a set of heterogeneous components (sensors, actuators, and controllers) that interact through a hierarchical communication network. We propose a methodology and a framework for design exploration and automatic synthesis of the communication network. We present how our approach can be applied to the design of control systems for intelligent buildings. The input specification of the control system includes (i) the constraints on the location of its components, which are imposed by the plant, (ii) the communication requirements among the components, and (iii) an estimation of the real-time constraints for the correct behavior of the algorithms implementing the control law. The output produces an implementation of the control networks that is obtained by combining elements from a pre-defined library of communication links, protocols, interfaces, and switches. The implementation is optimal in the sense that it satisfies the given specification while minimizing an objective function that captures the overall cost of the network implementation.
BibTeX
@inproceedings{pinto_communication_2007,
author = {Pinto, Alessandro and Carloni, Luca P and
Sangiovanni-Vincentelli, Alberto L},
title = {A Communication Synthesis Infrastructure for Heterogeneous
Networked Control Systems and Its Application to Building Automation
and Control},
booktitle = {Proceedings of the 7th ACM \& IEEE international
conference on Embedded software},
pages = {21-29},
date = {2007}
}
Paper
2006
Interchange semantics for hybrid system models
Alessandro Pinto, Luca P Carloni, Roberto Passerone, Alberto Sangiovanni-Vincentelli
Proc. of 5th MATHMODJournal article
Abstract
We propose an interchange format for hybrid systems to allow tool interoperability and seamless exchange of information among the hybrid system research community. The need of an interchange format is clear as the tools that have been developed so far use different modeling assumptions and semantics. In our approach, we focus on the semantics of the interchange format as we believe that only using a well-defined semantics will allow developing translation mechanisms from one tool to another that have guaranteed correctness properties. A unique, precise model of computation would make it impossible to support a variety of models that can be radically different. Hence, we use an “abstract semantics” in the sense that it can be refined to yield any model of computation, or “concrete semantics”, which, in turn, is associated to the existing languages that are used to specify hybrid systems. We show how leveraging its abstract semantics, the interchange format can be used to capture the essential information across different modeling approaches and how such information can be effectively used in the translation process
BibTeX
@article{pinto_interchange_2006-1,
author = {Pinto, Alessandro and Carloni, Luca P and Passerone, Roberto
and Sangiovanni-Vincentelli, Alberto},
title = {Interchange Semantics for Hybrid System Models},
journal = {Proc. of 5th MATHMOD},
date = {2006}
}
Paper
Slides
2006
Interchange format for hybrid systems: Abstract semantics
Alessandro Pinto, Luca P Carloni, Roberto Passerone, Alberto Sangiovanni-Vincentelli
International Workshop on Hybrid Systems: Computation and ControlConference paper
Abstract
In [1] we advocated the need for an interchange format for hybrid systems that enables the integration of design tools coming from many different research communities. In deriving such interchange format the main challenge is to define a language that, while presenting a particular formal semantics, remains general enough to accommodate the translation across the various modeling approaches used in the existing tools. In this paper we give a formal definition of the syntax and semantics for the proposed interchange format. In doing so, we clearly separate the structure of a hybrid system from the semantics attached to it. The semantics can be considered an “abstract semantics” in the sense that it can be refined to yield the model of computation, or “concrete semantics”, which, in turn, is associated to the existing languages that are used to specify hybrid systems. We show how the interchange format can be used to capture the essential information across different modeling approaches and how such information can be used in the translation process.
BibTeX
@inproceedings{pinto_interchange_2006,
author = {Pinto, Alessandro and Carloni, Luca P and Passerone, Roberto
and Sangiovanni-Vincentelli, Alberto},
publisher = {Springer},
title = {Interchange Format for Hybrid Systems: {Abstract} Semantics},
booktitle = {International Workshop on Hybrid Systems: Computation and
Control},
pages = {491-506},
date = {2006}
}
Paper
2006
Languages and tools for hybrid systems design
Luca P Carloni, Roberto Passerone, Alessandro Pinto, Alberto L Sangiovanni-Vincentelli, others
Foundations and Trends® in Electronic Design AutomationJournal article
Abstract
The explosive growth of embedded electronics is bringing information and control systems of increasing complexity to every aspects of our lives. The most challenging designs are safety-critical systems, such as transportation systems (e.g., airplanes, cars, and trains), industrial plants and health care monitoring. The difficulties reside in accommodating constraints both on functionality and implementation. The correct behavior must be guaranteed under diverse states of the environment and potential failures; implementation has to meet cost, size, and power consumption requirements. The design is therefore subject to extensive mathematical analysis and simulation. However, traditional models of information systems do not interface well to the continuous evolving nature of the environment in which these devices operate. Thus, in practice, different mathematical representations have to be mixed to analyze the overall behavior of the system. Hybrid systems are a particular class of mixed models that focus on the combination of discrete and continuous subsystems. There is a wealth of tools and languages that have been proposed over the years to handle hybrid systems. However, each tool makes different assumptions on the environment, resulting in somewhat different notions of hybrid system. This makes it difficult to share information among tools. Thus, the community cannot maximally leverage the substantial amount of work that has been directed to this important topic. In this paper, we review and compare hybrid system tools by highlighting their differences in terms of their underlying semantics, expressive power and mathematical mechanisms. We conclude our review with a comparative summary, which suggests the need for a unifying approach to hybrid systems design. As a step in this direction, we make the case for a semantic-aware interchange format, which would enable the use of joint techniques, make a formal comparison between different approaches possible, and facilitate exporting and importing design representations.
BibTeX
@article{carloni_languages_2006,
author = {Carloni, Luca P and Passerone, Roberto and Pinto, Alessandro
and Sangiovanni-Vincentelli, Alberto L and {others}},
publisher = {Now Publishers, Inc.},
title = {Languages and Tools for Hybrid Systems Design},
journal = {Foundations and Trends® in Electronic Design Automation},
volume = {1},
number = {1–2},
pages = {1-193},
date = {2006}
}
Paper
2006
System level design paradigms: Platform-based design and communication synthesis
Alessandro Pinto, Alvise Bonivento, Allberto L Sangiovanni-Vincentelli, Roberto Passerone, Marco Sgroi
ACM Transactions on Design Automation of Electronic Systems (TODAES)Journal article
Abstract
Embedded system level design must be based on paradigms that make formal foundations and unification a cornerstone of their construction. Platform-Based designs and communication synthesis are important components of the paradigm shift we advocate.Communication synthesis is a fundamental productivity tool in a design methodology where reuse is enforced. Communication design in a reuse methodology starts with a set of functional requirements and constraints on the interaction among components and then proceeds to build protocols, topology, and physical implementations that satisfy requirements and constraints while optimizing appropriate measures of efficiency of the implementation. Maximum efficiency can be reached when the communication specifications are entered at high levels of abstraction and the design process optimizes the implementation from this specification. Unfortunately, this process is very difficult if it is not cast in a rigorous framework. Platform-Based design helps define a successive refinement process where each step can be carried out automatically and optimized appropriately. We present two cases, an on-chip and a wireless sensor network design, where the resulting methodology gave encouraging results.
BibTeX
@article{pinto_system_2006,
author = {Pinto, Alessandro and Bonivento, Alvise and
Sangiovanni-Vincentelli, Allberto L and Passerone, Roberto and
Sgroi, Marco},
publisher = {ACM New York, NY, USA},
title = {System Level Design Paradigms: {Platform-based} Design and
Communication Synthesis},
journal = {ACM Transactions on Design Automation of Electronic Systems
(TODAES)},
volume = {11},
number = {3},
pages = {537-563},
date = {2006}
}
Paper
2005
Metropolis: A design environment for heterogeneous systems
Felice Balarin, Harry Hsieh, Luciano Lavagno, Claudio Passerone, Alessandro Pinto, Alberto Sangiovanni-Vincentelli, Yosinori Watanabe, Guang Yang
Multiprocessor systems-on-chipsBook chapter
BibTeX
@inbook{balarin2005metropolis,
author = {Balarin, Felice and Hsieh, Harry and Lavagno, Luciano and
Passerone, Claudio and Pinto, Alessandro and
Sangiovanni-Vincentelli, Alberto and Watanabe, Yosinori and Yang,
Guang},
publisher = {Elsevier},
title = {Metropolis: {A} Design Environment for Heterogeneous Systems},
booktitle = {Multiprocessor systems-on-chips},
pages = {465-496},
date = {2005}
}
2005
On the partitioning of syntax and semantics for hybrid systems tools
Jonathan Sprinkle, Aaron D Ames, Alessandro Pinto, Haiyang Zheng, S Shankar Sastry
Proceedings of the 44th IEEE Conference on Decision and ControlConference paper
Abstract
Interchange formats are notoriously difficult to finish. That is, once one is developed, it is highly nontrivial to prove (or disprove) generality, and difficult at best to gain acceptance from all major players in the application domain. This paper addresses such a problem for hybrid systems, but not from the perspective of a tool interchange format, but rather that of tool availability in a toolbox. Through the paper we explain why we think this is a good approach for hybrid systems, and we also analyze the domain of hybrid systems to discern the semantic partitions that can be formed to yield a classification of tools based on their semantics. These discoveries give us the foundation upon which to build semantic capabilities, and to guarantee operational interaction between tools based on matched operational semantics.
BibTeX
@inproceedings{sprinkle_partitioning_2005,
author = {Sprinkle, Jonathan and Ames, Aaron D and Pinto, Alessandro
and Zheng, Haiyang and Sastry, S Shankar},
publisher = {IEEE},
title = {On the Partitioning of Syntax and Semantics for Hybrid
Systems Tools},
booktitle = {Proceedings of the 44th IEEE Conference on Decision and
Control},
pages = {4694-4699},
date = {2005}
}
Paper
2005
Interchange formats for hybrid systems: Review and proposal
Alessandro Pinto, Alberto L Sangiovanni-Vincentelli, Luca P Carloni, Roberto Passerone
International Workshop on Hybrid Systems: Computation and ControlConference paper
Abstract
Interchange formats have been the backbone of the EDA industry for several years. They are used as a way of helping the development of design flows that integrate foreign tools using formats with different syntax and, more importantly, different semantics. The need for integrating tools coming from different communities is even more severe for hybrid systems because of the relative immaturity of the field and the intrinsic difficulty of the mathematical underpinnings. In this paper, we provide a discussion about interchange formats for hybrid systems, we survey the approaches used by different tools for analysis (simulation and formal verification) and synthesis of hybrid systems, and we give a recommendation for an interchange format for hybrid systems based on the METROPOLIS metamodel. The proposed interchange format has rigorous semantics and can accommodate the translation to and from the formats of the tools we have surveyed while providing a formal reasoning framework.
BibTeX
@inproceedings{pinto_interchange_2005,
author = {Pinto, Alessandro and Sangiovanni-Vincentelli, Alberto L and
Carloni, Luca P and Passerone, Roberto},
publisher = {Springer},
title = {Interchange Formats for Hybrid Systems: {Review} and
Proposal},
booktitle = {International Workshop on Hybrid Systems: Computation and
Control},
pages = {526-541},
date = {2005}
}
Paper
2005
Embedded system education: A new paradigm for engineering schools?
Alberto Luigi Sangiovanni-Vincentelli, Alessandro Pinto
ACM SIGBED ReviewJournal article
Abstract
Embedded systems are emerging as an essential component of modern electronic products. Embedded system design problems are posing challenges that involve entirely new skills for engineers. These skills are related to the combination of traditionally disjoint engineering disciplines. There is a shared concern that today’s educational systems are not providing the appropriate foundations for embedded systems. We believe a new education paradigm is needed.We will argue this point using the example of an emerging curriculum on embedded systems at the University of California at Berkeley. This curriculum is the result of a distillation process of more than ten years of intense research work. We will present the considerations that are driving the curriculum development and we review our undergraduate and graduate program. In particular, we describe in detail a graduate class (EECS249: Design of Embedded Systems: Modeling, Validation and Synthesis) that has been taught for six years. A common feature of our education agenda is the search for fundamentals of embedded system science rather than embedded system design techniques, an approach that today is rather unique.
BibTeX
@article{sangiovanni-vincentelli_embedded_2005,
author = {Sangiovanni-Vincentelli, Alberto Luigi and Pinto,
Alessandro},
publisher = {ACM New York, NY, USA},
title = {Embedded System Education: {A} New Paradigm for Engineering
Schools?},
journal = {ACM SIGBED Review},
volume = {2},
number = {4},
pages = {5-14},
date = {2005}
}
Paper
2005
A formal approach to system level design: Metamodels and unified design environments
Felice Balarin, Roberto Passerone, Alessandro Pinto, Alberto L Sangiovanni-Vincentelli
Proceedings. Second ACM and IEEE International Conference on Formal Methods and Models for Co-Design, 2005. MEMOCODE’05.Conference paper
Abstract
The debate about efficient methods for hardware-software co-design has taken interesting turns over the years. In this paper, we argue that the essential problems to solve are prior to the decision on how to partition the system in hardware-software. We present a formal platform-based design method we have proposed over the years and a design environment, Metropolis, supporting the methodology, which starts by capturing the design specifications at the highest level of abstraction and then proceed toward an efficient implementation by subsequent refinement steps. We present the modeling strategy used in Metropolis based on formal semantics that is general enough to support the models of computation proposed so far and that facilitates the creation of new ones. Nonfunctional and declarative constraints can also be captured using a logic language.
BibTeX
@inproceedings{balarin_formal_2005,
author = {Balarin, Felice and Passerone, Roberto and Pinto, Alessandro
and Sangiovanni-Vincentelli, Alberto L},
publisher = {IEEE},
title = {A Formal Approach to System Level Design: {Metamodels} and
Unified Design Environments},
booktitle = {Proceedings. Second ACM and IEEE International Conference
on Formal Methods and Models for Co-Design, 2005. MEMOCODE’05.},
pages = {155-163},
date = {2005}
}
Paper
2005
An overview of embedded system design education at Berkeley
Alberto L Sangiovanni-Vincentelli, Alessandro Pinto
ACM Transactions on Embedded Computing Systems (TECS)Journal article
Abstract
Embedded systems have been a traditional area of strength in the research agenda of the University of California at Berkeley. In parallel to this effort, a pattern of graduate and undergraduate classes has emerged that is the result of a distillation process of the research results. In this paper, we present the considerations that are driving our curriculum development and we review our undergraduate and graduate program. In particular, we describe in detail a graduate class (EECS249: Design of Embedded Systems: Modeling, Validation and Synthesis) that has been taught for six years. A common feature of our education agenda is the search for fundamentals of embedded system science rather than embedded system design techniques, an approach that today is rather unique.
BibTeX
@article{sangiovanni-vincentelli_overview_2005,
author = {Sangiovanni-Vincentelli, Alberto L and Pinto, Alessandro},
publisher = {ACM New York, NY, USA},
title = {An Overview of Embedded System Design Education at
{Berkeley}},
journal = {ACM Transactions on Embedded Computing Systems (TECS)},
volume = {4},
number = {3},
pages = {472-499},
date = {2005}
}
Paper
2003
Efficient synthesis of networks on chip
Alessandro Pinto, Luca P Carloni, Alberto L Sangiovanni-Vincentelli
Proceedings 21st International Conference on Computer DesignConference paper
Abstract
We propose an efficient heuristic for the constraint-driven communication synthesis (CDCS) of on-chip communication networks. The complexity of the synthesis problems comes from the number of constraints that have to be considered. We propose to cluster constraints to reduce the number that needs to be considered by the optimization algorithm. Then a quadratic programming approach is used to solve the communication synthesis problem with the clustered constraints. We provide an analytical model that justifies our choice of the clustering cost function and we discuss a set of experiments showing the effectiveness of the overall approach with respect to the exact algorithm.
BibTeX
@inproceedings{pinto_efficient_2003,
author = {Pinto, Alessandro and Carloni, Luca P and
Sangiovanni-Vincentelli, Alberto L},
publisher = {IEEE},
title = {Efficient Synthesis of Networks on Chip},
booktitle = {Proceedings 21st International Conference on Computer
Design},
pages = {146-150},
date = {2003}
}
Paper
2002
Constraint-driven communication synthesis
Alessandro Pinto, Luca P Carloni, Alberto L Sangiovanni-Vincentelli
Proceedings of the 39th annual Design Automation ConferenceConference paper
Abstract
Constraint-driven Communication Synthesis enables the automatic design of the communication architecture of a complex system from a library of pre-defined Intellectual Property (IP) components. The key communication parameters that govern all the point-to-point interactions among system modules are captured as a set of arc constraints in the communication constraint graph. Similarly, the communication features offered by each of the components available in the IP communication library are captured as a set of feature resources together with its cost figures. Then, every communication architecture that can be built using the available components while satisfying all constraints is implicitly considered (as an implementation graph matching the constraint graph) to derive the optimum design solution with respect to the desired cost figure. The corresponding constrained optimization problem is efficiently solved by a novel algorithm that is presented here together with its rigorous theoretical foundations.
BibTeX
@inproceedings{pinto_constraint-driven_2002,
author = {Pinto, Alessandro and Carloni, Luca P and
Sangiovanni-Vincentelli, Alberto L},
title = {Constraint-Driven Communication Synthesis},
booktitle = {Proceedings of the 39th annual Design Automation
Conference},
pages = {783-788},
date = {2002}
}
Paper
No publications match these filters.
No matching items