View source for SURF 2023: Formal compositional design of electro-mechanical systems

'''[[SURF 2023|2023 SURF]] project description'''

* Mentor: Richard Murray
* Co-mentor: Inigo Incer

[[File:SURF2023-CBD.png|400px|thumb|right|Figure 1. Composition and quotient operations for assume-guarantee contracts]]

Practitioners often rank the handling of specifications as one of the top challenges of systems engineering. Requirements expressed in natural languages can be conflicting, incomplete, unrealizable, etc. One way to alleviate this problem and the miscommunications it can produce in the supply chain is by making specifications formal (i.e., having well-defined mathematical meaning) and providing means for handling these specifications algebraically and computationally.

Contract-based design [1,2] has emerged as a methodology to design and analyze complex systems formally. In contract-based design, every component in a system is represented using an assume-guarantee specification. A rich contract algebra allows us to compute the specification of a system given the specifications of the subsystems. Conversely, given the specification of a system and the specification of a subsystem, we can compute the specification of a missing component that would allow the system to meet its objective [3]. These two processes, namely, composition and quotient are shown in Figure 1.

In this project, we will model an electromechanical system (e.g., an engine, a turbine) using assume-guarantee specifications. The specifications and guarantees of each component will be expressed using linear inequalities. Using contract-based design and tools currently in development, you will be able to compose system specifications and to take quotients.

Programming in python will be part of this project. As a result, you should be familiar with a programming language. Your background should enable you to reason about the design and analysis of complex electromechanical systems, such as engines or turbines. Background in formal methods is not required, but will be helpful.

References
# Benveniste, A., Caillaud, B., Nickovic, D., Passerone, R., Raclet, J.B., Reinkemeier, P., Sangiovanni-Vincentelli, A., Damm, W., Henzinger, T.A., Larsen, K.G.: [https://www.nowpublishers.com/article/Details/EDA-053 Contracts for system design]. Foundations and Trends in Electronic Design Automation 12(2-3), 124–400 (2018)
# Nuzzo, P., Xu, H., Ozay, N., Finn, J., Sangiovanni-Vincentelli, A., Murray, R., Donzé, A., Seshia, S.: [https://ieeexplore.ieee.org/abstract/document/6690099 A Contract-Based Methodology for Aircraft Electric Power System Design], in IEEE Access, vol. 2, pp. 1-25, 2014, doi: 10.1109/ACCESS.2013.2295764.
# Incer, I., Sangiovanni-Vincentelli, A., Lin, C. -W., Kang, E.: [https://ieeexplore.ieee.org/abstract/document/8556872 Quotient for Assume-Guarantee Contracts], in Proceedings of the 16th ACM/IEEE International Conference on Formal Methods and Models for System Design (MEMOCODE), 2018, pp. 1-11, doi: 10.1109/MEMCOD.2018.8556872.