Pierluigi Nuzzo
Skip Abstract Section
Abstract
We present an assume-guarantee contract framework for cyber-physical system design under probabilistic requirements. Given a stochastic linear system and a set of requirements captured by bounded Stochastic Signal Temporal Logic (StSTL) contracts, we propose algorithms to check contract compatibility, consistency, and refinement, and generate a sequence of control inputs that satisfies a contract. We leverage encodings of the verification and control synthesis tasks into mixed integer optimization problems, and conservative approximations of probabilistic constraints that produce sound and tractable problem formulations. We illustrate the effectiveness of our approach on three case studies, including the design of controllers for aircraft power distribution networks.
- 2018. Stochastic Contract-based Analysis and Synthesis. Retrieved from https://github.com/nuzzo/SCAnS.Google Scholar
- Tobias Achterberg and Roland Wunderling. 2013. Mixed integer programming: Analyzing 12 years of progress. In Facets of Combinatorial Optimization. Springer, 449--481.Google Scholar
- Alberto Bemporad and Manfred Morari. 1999. Control of systems integrating logic, dynamics, and constraints. Automatica 35, 3 (1999), 407--427. Google ScholarDigital Library
- Albert Benveniste, Benoît Caillaud, Alberto Ferrari, Leonardo Mangeruca, Roberto Passerone, and Christos Sofronis. 2008. Multiple viewpoint contract-based specification and design. In Formal Methods for Components and Objects. Springer-Verlag, Berlin, Germany, 200--225. Google ScholarDigital Library
- Albert Benveniste, Benoît Caillaud, Dejan Nickovic, Roberto Passerone, Jean-Baptiste Raclet, Philipp Reinkemeier, Alberto Sangiovanni-Vincentelli, Werner Damm, Thomas Henzinger, and Kim Guldstrand Larsen. 2012. Contracts for System Design. Rapport de recherche RR-8147. INRIA. 65 pages.Google Scholar
- Stephen Bradley, Arnoldo Hax, and Thomas Magnanti. 1977. Applied Mathematical Programming. Addison Wesley.Google Scholar
- Benoît Caillaud, Benoît Delahaye, Kim G. Larsen, Axel Legay, Mikkel L. Pedersen, and Andrzej Wąsowski. 2010. Compositional design methodology with constraint Markov chains. In Int. Conf. Quantitative Evaluation of Systems. 123--132. Google ScholarDigital Library
- Alessandro Cimatti and Stefano Tonetta. 2015. Contracts-refinement proof system for component-based embedded systems. Science of Computer Programming 97, Part 3 (2015), 333--348. Google ScholarDigital Library
- Edmund M. Clarke, E. Allen Emerson, and A. Prasad Sistla. 1986. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems (TOPLAS) 8, 2 (1986), 244--263. Google ScholarDigital Library
- E. M. Clarke, O. Grumberg, and D. A. Peled. 2008. Model Checking. The MIT Press, Cambridge, MA.Google Scholar
- Luca de Alfaro and Thomas A. Henzinger. 2001. Interface automata. In Proc. Symp. Foundations of Software Engineering. ACM Press, 109--120. Google ScholarDigital Library
- Carlos E. de Souza, Alexandre Trofino, and Karina A. Barbosa. 2006. Mode-independent filters for Markovian jump linear systems. IEEE Trans. Automatic Control 51, 11 (2006), 1837--1841.Google ScholarCross Ref
- Benoît Delahaye, Benoît Caillaud, and Axel Legay. 2010. Probabilistic contracts: A compositional reasoning methodology for the design of stochastic systems. In Int. Conf. Application of Concurrency to System Design. 223--232. Google ScholarDigital Library
- Benoît Delahaye, Joost-Pieter Katoen, Kim G. Larsen, Axel Legay, Mikkel L. Pedersen, Falak Sher, and Andrzej Wąsowski. 2011. Abstract probabilistic automata. In Int. Workshop Verification, Model Checking, and Abstract Interpretation. Springer, 324--339. Google ScholarDigital Library
- Benoît Delahaye, Kim G. Larsen, Axel Legay, Mikkel L. Pedersen, and Andrzej Wąsowski. 2011. APAC: A tool for reasoning about abstract probabilistic automata. (2011).Google Scholar
- Rick Durrett. 2010. Probability: Theory and Examples. Cambridge University Press. Google ScholarDigital Library
- Nicola Elia. 2005. Remote stabilization over fading channels. Systems 8 Control Letters 54, 3 (2005), 237--249.Google Scholar
- S. S. Farahani, R. Majumdar, V. S. Prabhu, and S. E. Z. Soudjani. 2017. Shrinking horizon model predictive control with chance-constrained signal temporal logic specifications. In Proc. American Control Conf. 1740--1746.Google ScholarCross Ref
- Shromona Ghosh, Dorsa Sadigh, Pierluigi Nuzzo, Vasumathi Raman, Alexandre Donze, Alberto Sangiovanni-Vincentelli, S. Shankar Sastry, and Sanjit A. Seshia. 2016. Diagnosis and repair for synthesis from signal temporal logic specifications.Google Scholar
- Gregor Gössler, Dana N. Xu, and Alain Girault. 2012. Probabilistic contracts for component-based design. Formal Methods in System Design 41, 2 (2012), 211--231. Google ScholarDigital Library
- Inc. Gurobi Optimization. 2015. Gurobi Optimizer Reference Manual. Retrieved from http://www.gurobi.com.Google Scholar
- Hans Hansson and Bengt Jonsson. 1994. A logic for reasoning about time and reliability. Formal Aspects of Computing 6, 5 (1994), 512--535.Google ScholarDigital Library
- Christopher M. Harris and Daniel M. Wolpert. 1998. Signal-dependent noise determines motor planning. Nature 394, 6695 (1998), 780--784.Google Scholar
- Antonio Iannopollo, Pierluigi Nuzzo, Stavros Tripakis, and Alberto L. Sangiovanni-Vincentelli. 2014. Library-based scalable refinement checking for contract-based design. In Proc. Design, Automation and Test in Europe. 1--6. Google ScholarDigital Library
- Marta Kwiatkowska, Gethin Norman, and David Parker. 2007. Stochastic model checking. In Formal Methods for the Design of Computer, Communication and Software Systems: Performance Evaluation (SFM’07) (Lecture Notes in Computer Science), M. Bernardo and J. Hillston (Eds.), Vol. 4486. Springer, 220--270. Google ScholarDigital Library
- Marta Kwiatkowska, Gethin Norman, and David Parker. 2011. PRISM 4.0: Verification of probabilistic real-time systems. In Proc. Int. Conf. Comput.-Aided Verification (Lecture Notes in Computer Science), G. Gopalakrishnan and S. Qadeer (Eds.), Vol. 6806. Springer, 585--591. Google ScholarDigital Library
- Marta Kwiatkowska, Gethin Norman, David Parker, and Hongyang Qu. 2010. Assume-guarantee verification for probabilistic systems. In Proc. Int. Conf. Tools and Algorithms for the Construction and Analysis of Systems (Lecture Notes in Computer Science), Vol. 6015. Springer, 23--37. Google ScholarDigital Library
- Jiwei Li, Pierluigi Nuzzo, Alberto Sangiovanni-Vincentelli, Yugeng Xi, and Dewei Li. 2017. Stochastic contracts for cyber-physical system design under probabilistic requirements. In Proc. Int. Conf. Formal Methods and Models for Co-Design. 5--14. Google ScholarDigital Library
- J. Löfberg. 2004. YALMIP: A toolbox for modeling and optimization in MATLAB. In Proc. IEEE Int. Symp. Computer Aided Control Systems Design. Taipei, Taiwan.Google ScholarCross Ref
- Mehdi Maasoumy, Pierluigi Nuzzo, Forrest Iandola, Maryam Kamgarpour, Alberto Sangiovanni-Vincentelli, and Claire Tomlin. 2013. Optimal load management system for aircraft electric power distribution. In Proc. Int. Conf. Decision and Control. IEEE, 2939--2945.Google ScholarCross Ref
- Oded Maler and Dejan Nickovic. 2004. Monitoring temporal properties of continuous signals. In Formal Modeling and Analysis of Timed Systems. 152--166.Google Scholar
- B. Meyer. 1992. Applying “design by contract.” Computer 25, 10 (Oct. 1992), 40--51. Google ScholarDigital Library
- Arkadi Nemirovski and Alexander Shapiro. 2006. Convex approximations of chance constrained programs. SIAM Journal on Optimization 17, 4 (2006), 969--996. Google ScholarDigital Library
- Pierluigi Nuzzo, Michele Lora, Yishai Feldman, and A. Sangiovanni-Vincentelli. 2018. CHASE: Contract-based requirement engineering for cyber-physical system design. In Proc. Design, Automation and Test in Europe. Dresden, Germany, 839--844.Google Scholar
- Pierluigi Nuzzo, Alberto Sangiovanni-Vincentelli, Davide Bresolin, Luca Geretti, and Tiziano Villa. 2015. A platform-based design methodology with contracts and related tools for the design of cyber-physical systems. Proc. IEEE 103, 11 (Nov. 2015), 2104--2132.Google ScholarCross Ref
- Pierluigi Nuzzo, Alberto Sangiovanni-Vincentelli, Xuening Sun, and Alberto Puggelli. 2012. Methodology for the design of analog integrated interfaces using contracts. IEEE Sensors Journal 12, 12 (2012), 3329--3345.Google ScholarCross Ref
- Pierluigi Nuzzo, Huan Xu, Necmiye Ozay, John B. Finn, Alberto L. Sangiovanni-Vincentelli, Richard M. Murray, Alexandre Donzé, and Sanjit A. Seshia. 2014. A contract-based methodology for aircraft electric power system design. IEEE Access 2 (2014), 1--25.Google ScholarCross Ref
- André Platzer. 2011. Stochastic differential dynamic logic for stochastic hybrid programs. In Int. Conf. Automated Deduction. 446--460. Google ScholarDigital Library
- Jean-Baptiste Raclet, Eric Badouel, Albert Benveniste, Benoît Caillaud, Axel Legay, and Roberto Passerone. 2009. Modal interfaces: Unifying interface automata and modal specifications. In Proc. ACM/IEEE Int. Conf. Embedded Software. 87--96. Google ScholarDigital Library
- Vasumathi Raman, Alexandre Donzé, Mehdi Maasoumy, Richard M. Murray, Alberto Sangiovanni-Vincentelli, and Sanjit A. Seshia. 2014. Model predictive control with signal temporal logic specifications. In Proc. Int. Conf. Decision and Control. IEEE, 81--87.Google Scholar
- Line Roald and Göran Andersson. 2018. Chance-constrained AC optimal power flow: Reformulations and efficient algorithms. IEEE Transactions on Power Systems 33, 3 (May 2018), 2906--2918.Google ScholarCross Ref
- Dorsa Sadigh and Ashish Kapoor. 2016. Safe control under uncertainty with probabilistic signal temporal logic. In Proc. of Robotics: Science and Systems (RSS’16).Google ScholarCross Ref
- Alberto Sangiovanni-Vincentelli, Werner Damm, and Roberto Passerone. 2012. Taming Dr. Frankenstein: Contract-based design for cyber-physical systems. European Journal of Control 18, 3 (2012), 217--238.Google ScholarCross Ref
- Behrooz Shahsavari, Mehdi Maasoumy, Alberto Sangiovanni-Vincentelli, and Roberto Horowitz. 2015. Stochastic model predictive control design for load management system of aircraft electrical power distribution. In Proc. American Control Conference. 3649--3655.Google ScholarCross Ref
- Wayne L. Winston. 2008. Operations Research: Applications 8 Algorithms. Thomson Business Press.Google Scholar
Index Terms
- Stochastic Assume-Guarantee Contracts for Cyber-Physical System Design
Recommendations
Stochastic contracts for cyber-physical system design under probabilistic requirements
MEMOCODE '17: Proceedings of the 15th ACM-IEEE International Conference on Formal Methods and Models for System DesignWe develop an assume-guarantee contract framework for the design of cyber-physical systems, modeled as closed-loop control systems, under probabilistic requirements. We use a variant of signal temporal logic, namely, Stochastic Signal Temporal Logic (...
Assume-guarantee testing
SAVCBS '05: Proceedings of the 2005 conference on Specification and verification of component-based systemsVerification techniques for component-based systems should ideally be able to predict properties of the assembled system through analysis of individual components before assembly. This work introduces such a modular technique in the context of testing. ...
Symbolic assume-guarantee reasoning through BDD learning
ICSE 2014: Proceedings of the 36th International Conference on Software EngineeringBoth symbolic model checking and assume-guarantee reasoning aim to circumvent the state explosion problem. Symbolic model checking explores many states simultaneously and reports numerous erroneous traces. Automated assume-guarantee reasoning, on the ...
Comments