research-article

Synthesis of live behaviour models

Authors:

Nicolás Roque D'Ippolito,

Victor Braberman,

Sebastián UchitelAuthors Info & Claims

FSE '10: Proceedings of the eighteenth ACM SIGSOFT international symposium on Foundations of software engineering

Pages 77 - 86

https://doi.org/10.1145/1882291.1882305

Published: 07 November 2010 Publication History

Abstract

We present a novel technique for synthesising behaviour models that works for an expressive subset of liveness properties and conforms to the foundational requirements engineering World/Machine model, dealing explicitly with assumptions on environment behaviour and distinguishing controlled and monitored actions. This is the first technique that conforms to what is considered best practice in requirements specifications: distinguishing prescriptive and descriptive assertions. Most previous attempts at using synthesis of behavioural models were restricted to handling only safety properties. Those that did support liveness were inadequate for synthesis of operational event based models as they did not include the bespoke distinction between system goals and environment assumptions.

References

[1]

E. Asarin, O. Maler, A. Pnueli, and J. Sifakis. Controller synthesis for timed automata. In Proc. SSC, pp. 469--474. 1998.

[2]

M. Autili, P. Inverardi, M. Tivoli, and D. Garlan. Synthesis of correct adaptors for protocol enhancement in component-based systems. Proc. SAVCBS, pp. 79, 2004.

[3]

P. Bertoli, A. Cimatti, M. Pistore, M. Roveri, and P. Traverso. MBP: a model based planner. In Proc. IJCAI Workshop on Planning under Uncertainty and Incomplete Information. 2001.

[4]

A. Bertolino, P. Inverardi, P. Pelliccione, and M. Tivoli. Automatic synthesis of behavior protocols for composable web-services. In Proc. FSE, pp. 141--150, 2009.

Digital Library

[5]

Y. Bontemps, P. Schobbens, and C. Löding. Synthesis of open reactive systems from scenario-based specifications. Fundamenta Informaticae, 62(2):139--169, 2004.

Digital Library

[6]

F. Dalpiaz, P. Giorgini, and J. Mylopoulos. An Architecture for Requirements-Driven Self-reconfiguration. In Proc. AISE, pp. 260. Springer, 2009.

Digital Library

[7]

C. Damas, B. Lambeau, and A. van Lamsweerde. Scenarios, goals, and state machines: a win-win partnership for model synthesis. In Proc. FSE, pp. 197--207, 2006

Digital Library

[8]

L. De Alfaro and T. Henzinger. Interface automata. ACM Software Engineering Notes, 26(5):120, 2001.

Digital Library

[9]

N. D'Ippolito. MTSA Tool., 2010. http://www.doc.ic.ac.uk/srdipi/fse2010/.

[10]

N. D'Ippolito, D. Fischbein, M. Chechik, and S. Uchitel. MTSA: The modal transition system analyser. In Proc. ASE, pp. 475--476, 2008.

Digital Library

[11]

D. Garlan, S. Cheng, A. Huang, B. Schmerl, and P. Steenkiste. Rainbow: Architecture-based self-adaptation with reusable infrastructure. Computer, pages 46--54, 2004.

Digital Library

[12]

D. Giannakopoulou and J. Magee. Fluent model checking for event-based systems. ACM Software Engineering Notes, 28(5):257--266, 2003.

Digital Library

[13]

F. Giunchiglia and P. Traverso. Planning as model checking. In Proc. ECP RAAP, pages 1--20, 2000.

Digital Library

[14]

W. Heaven, D. Sykes, J. Magee, and J. Kramer. A Case Study in Goal-Driven Architectural Adaptation. In Proc. SEfSAS, page 127. Springer, 2009.

Digital Library

[15]

C. Hoare. Communicating sequential processes. CACM, 21(8):677, 1978.

Digital Library

[16]

M. Jackson. Software Specifications and Requirements: a lexicon of practice, principles and prejudices. Addison-Wesley, 1995.

Digital Library

[17]

M. Jackson. The world and the machine. In Proc. ICSE, pp. 283--292, 1995.

Digital Library

[18]

M. Jurdziński. Small progress measures for solving parity games. In Proc. STACS, LNCS 1770, pp. 290--301, 2000. Springer-Verlag.

[19]

R. Kazhamiakin, M. Pistore, and M. Roveri. "Formal Verification of Requirements using SPIN: A Case Study on Web Services". In Proc. SEFM, 2004.

Digital Library

[20]

R. Keller. "Formal Verification of Parallel Programs". CACM, 19(7):371--384, 1976.

Digital Library

[21]

A. V. Lamsweerde. Goal-oriented requirements engineering: A guided tour. Requirements Engineering, IEEE International Conference on, 0:0249, 2001.

Digital Library

[22]

E. Letier and A. Van Lamsweerde. Agent-based tactics for goal-oriented requirements elaboration. In Proc. ICSE, volume 24, pages 83--93, 2002.

Digital Library

[23]

C. Lewerentz and T. Lindner, editors. Formal Development of Reactive Systems - Case Study Production Cell, LNCS 891. Springer, 1995.

Digital Library

[24]

J. Magee and J. Kramer. Concurrency: state models & Java programs. Wiley New York, 2006.

Digital Library

[25]

Z. Manna and A. Pnueli. The temporal logic of reactive and concurrent systems: Specification. Springer, 1992.

Digital Library

[26]

D. L. Parnas and J. Madey. Functional documents for computer systems. SCP, 25(1):41--61, 1995.

Digital Library

[27]

N. Piterman, A. Pnueli, and Y. Sa'ar. Synthesis of reactive (1) designs. In Proc. VMCAI, LNCS 3855, pp. 364--381, 2006.

Digital Library

[28]

A. Pnueli and R. Rosner. On the synthesis of a reactive module. In Proc. POPL, pp. 179--190, 1989.

Digital Library

[29]

P. Ramadge and W. Wonham. The control of discrete event systems. Proc. of the IEEE, 77(1):81--98, 1989.

[30]

S. Russell and P. Norvig. Artificial intelligence: a modern approach. New Jersey, 1995.

Digital Library

[31]

D. Sykes, W. Heaven, J. Magee, and J. Kramer. Plan-directed architectural change for autonomous systems. In Proc. FSE, pp. 15--21, 2007.

Digital Library

[32]

S. Uchitel, G. Brunet, and M. Chechik. Behaviour model synthesis from properties and scenarios. In Proc. ICSE, pp. 34--43, 2007.

Digital Library

[33]

A. van Lamsweerde and E. Letier. "Handling Obstacles in Goal-Oriented Requirements Engineering". Trans. on SE, 26(10):978--1005, 2000.

Digital Library

Cited By

Reniers MKeiren J(2024)Validation of supervisory control synthesis tool CIF using model checker mCRL22024 IEEE 20th International Conference on Automation Science and Engineering (CASE)10.1109/CASE59546.2024.10711749(1437-1442)Online publication date: 28-Aug-2024
https://doi.org/10.1109/CASE59546.2024.10711749
Asteasuain F(2023)Formal Validation of Software for Nano Satellite MissionsRevista Abierta de Informática Aplicada10.59471/raia2023537:1(12-23)Online publication date: 30-Jun-2023
https://doi.org/10.59471/raia202353
Hu MXia JZhang MChen XMallet FChen M(2023)Automated Synthesis of Safe Timing Behaviors for Requirements Models Using CCSLIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems10.1109/TCAD.2023.328541242:12(5127-5140)Online publication date: Dec-2023
https://doi.org/10.1109/TCAD.2023.3285412
Show More Cited By

Index Terms

Synthesis of live behaviour models
1. Software and its engineering

Recommendations

Synthesis of live behaviour models for fallible domains
ICSE '11: Proceedings of the 33rd International Conference on Software Engineering

We revisit synthesis of live controllers for event-based operational models. We remove one aspect of an idealised problem domain by allowing to integrate failures of controller actions in the environment model. Classical treatment of failures through ...
Coloured Petri Nets and CPN Tools for modelling and validation of concurrent systems

Coloured Petri Nets (CPNs) is a language for the modelling and validation of systems in which concurrency, communication, and synchronisation play a major role. Coloured Petri Nets is a discrete-event modelling language combining Petri nets with the ...
Coloured Petri Nets and CPN Tools for modelling and validation of concurrent systems
Abstract
Coloured Petri Nets (CPNs) is a language for the modelling and validation of systems in which concurrency, communication, and synchronisation play a major role. Coloured Petri Nets is a discrete-event modelling language combining Petri nets with ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

FSE '10: Proceedings of the eighteenth ACM SIGSOFT international symposium on Foundations of software engineering

November 2010

302 pages

ISBN:9781605587912

DOI:10.1145/1882291

General Chair:
Gruia-Catalin Roman
Washington University in St. Louis, USA
,
Program Chair:
André van der Hoek
University of California, Irvine, USA

Copyright © 2010 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

SIGSOFT: ACM Special Interest Group on Software Engineering

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 07 November 2010

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

SIGSOFT/FSE'10

Sponsor:

SIGSOFT

SIGSOFT/FSE'10: 18th ACM SIGSOFT Symposium on the Foundations of Software Engineering

November 7 - 11, 2010

New Mexico, Santa Fe, USA

Acceptance Rates

Overall Acceptance Rate 17 of 128 submissions, 13%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

51
Total Citations
View Citations
381
Total Downloads

Downloads (Last 12 months)11
Downloads (Last 6 weeks)2

Reflects downloads up to 24 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Reniers MKeiren J(2024)Validation of supervisory control synthesis tool CIF using model checker mCRL22024 IEEE 20th International Conference on Automation Science and Engineering (CASE)10.1109/CASE59546.2024.10711749(1437-1442)Online publication date: 28-Aug-2024
https://doi.org/10.1109/CASE59546.2024.10711749
Asteasuain F(2023)Formal Validation of Software for Nano Satellite MissionsRevista Abierta de Informática Aplicada10.59471/raia2023537:1(12-23)Online publication date: 30-Jun-2023
https://doi.org/10.59471/raia202353
Hu MXia JZhang MChen XMallet FChen M(2023)Automated Synthesis of Safe Timing Behaviors for Requirements Models Using CCSLIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems10.1109/TCAD.2023.328541242:12(5127-5140)Online publication date: Dec-2023
https://doi.org/10.1109/TCAD.2023.3285412
Arioka YYamauchi TTei K(2023)Pre-controller Synthesis for Runtime Controller Synthesis2023 IEEE 13th International Conference on Control System, Computing and Engineering (ICCSCE)10.1109/ICCSCE58721.2023.10237143(161-166)Online publication date: 25-Aug-2023
https://doi.org/10.1109/ICCSCE58721.2023.10237143
Schmuck AThejaswini KSağlam INayak S(2023)Solving Two-Player Games Under Progress AssumptionsVerification, Model Checking, and Abstract Interpretation10.1007/978-3-031-50524-9_10(208-231)Online publication date: 30-Dec-2023
https://doi.org/10.1007/978-3-031-50524-9_10
Yamauchi THirano TLi JKawasaki TChen YTsuge AOkoshi TNakazawa JYoshioka NPalaiokrassas GLitke ATei K(2021)A Development Method for Safe Node-RED Systems using Discrete Controller Synthesis2021 IEEE International Conferences on Internet of Things (iThings) and IEEE Green Computing & Communications (GreenCom) and IEEE Cyber, Physical & Social Computing (CPSCom) and IEEE Smart Data (SmartData) and IEEE Congress on Cybermatics (Cybermatics)10.1109/iThings-GreenCom-CPSCom-SmartData-Cybermatics53846.2021.00033(130-137)Online publication date: Dec-2021
https://doi.org/10.1109/iThings-GreenCom-CPSCom-SmartData-Cybermatics53846.2021.00033
Seow K(2021)Supervisory Control of Fair Discrete-Event Systems: A Canonical Temporal Logic FoundationIEEE Transactions on Automatic Control10.1109/TAC.2020.303715666:11(5269-5282)Online publication date: Nov-2021
https://doi.org/10.1109/TAC.2020.3037156
Zudaire SGorostiaga FSanchez CSchneider GUchitel S(2021)Assumption Monitoring Using Runtime Verification for UAV Temporal Task Plan Executions2021 IEEE International Conference on Robotics and Automation (ICRA)10.1109/ICRA48506.2021.9561671(6824-6830)Online publication date: 30-May-2021
https://doi.org/10.1109/ICRA48506.2021.9561671
Hirano TTei KAizawa KHoniden S(2021)Differential Controller Synthesis at Runtime Using Changed Parts of Environment Model2021 IEEE 8th International Conference on Industrial Engineering and Applications (ICIEA)10.1109/ICIEA52957.2021.9436711(91-100)Online publication date: 23-Apr-2021
https://doi.org/10.1109/ICIEA52957.2021.9436711
Li JTei KHoniden S(2021)Identifying Achievable Goals for Adaptive Replanning Against Runtime Environment ChangeIntelligent Systems Design and Applications10.1007/978-3-030-71187-0_87(945-955)Online publication date: 3-Jun-2021
https://doi.org/10.1007/978-3-030-71187-0_87
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents