\n \n \n
\n
\n\n \n \n \n \n \n \n Incorporating Monitors in Reactive Synthesis without Paying the Price.\n \n \n \n \n\n\n \n Azzopardi, S.; Piterman, N.; and Schneider, G.\n\n\n \n\n\n\n 2021.\n
\n\n
\n\n
\n\n
\n\n \n \n
Paper\n \n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n \n \n 2 downloads\n \n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n
\n
@misc{azzopardi2021incorporating,\n title={Incorporating Monitors in Reactive Synthesis without Paying the Price}, \n author={Shaun Azzopardi and Nir Piterman and Gerardo Schneider},\n year={2021},\n eprint={2107.00929},\n archivePrefix={arXiv},\n primaryClass={cs.LO},\n booktitle={arXiv},\n url={https://arxiv.org/abs/2107.00929}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n
\n\n \n \n \n \n \n \n On the Specification and Monitoring of Timed Normative Systems.\n \n \n \n \n\n\n \n Azzopardi, S.; Pace, G.; Schapachnik, F.; and Schneider, G.\n\n\n \n\n\n\n In Feng, L.; and Fisman, D., editor(s),
Runtime Verification (RV), pages 81–99, Cham, 2021. Springer International Publishing\n
\n\n
\n\n
\n\n
\n\n \n \n
Paper\n \n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n \n \n abstract \n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n
\n
@inproceedings{rv21,\nauthor="Azzopardi, Shaun\nand Pace, Gordon\nand Schapachnik, Fernando\nand Schneider, Gerardo",\neditor="Feng, Lu\nand Fisman, Dana",\ntitle="On the Specification and Monitoring of Timed Normative Systems",\nbooktitle="Runtime Verification (RV)",\nyear="2021",\npublisher="Springer International Publishing",\naddress="Cham",\npages="81--99",\nabstract="In this article we explore different issues and design choices that arise when considering how to fully embrace timed aspects in the formalisation of normative systems, e.g., by using deontic modalities, looking primarily through the lens of monitoring. We primarily focus on expressivity and computational aspects, discussing issues such as duration, superposition, conflicts, attempts, discharge, and complexity, while identifying semantic choices which arise and the challenges these pose for full monitoring of legal contracts.",\nisbn="978-3-030-88494-9",\nurl="https://gupea.ub.gu.se/bitstream/handle/2077/74148/309362.pdf?sequence=1"\n}\n\n
\n
\n\n\n
\n In this article we explore different issues and design choices that arise when considering how to fully embrace timed aspects in the formalisation of normative systems, e.g., by using deontic modalities, looking primarily through the lens of monitoring. We primarily focus on expressivity and computational aspects, discussing issues such as duration, superposition, conflicts, attempts, discharge, and complexity, while identifying semantic choices which arise and the challenges these pose for full monitoring of legal contracts.\n
\n\n\n
\n\n\n
\n
\n\n \n \n \n \n \n \n Incorporating Monitors in Reactive Synthesis Without Paying the Price.\n \n \n \n \n\n\n \n Azzopardi, S.; Piterman, N.; and Schneider, G.\n\n\n \n\n\n\n In Hou, Z.; and Ganesh, V., editor(s),
Automated Technology for Verification and Analysis, pages 337–353, Cham, 2021. Springer International Publishing\n
\n\n
\n\n
\n\n
\n\n \n \n
Paper\n \n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n \n \n abstract \n \n\n \n \n \n 2 downloads\n \n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n
\n
@inproceedings{atva21,\nauthor="Azzopardi, Shaun\nand Piterman, Nir\nand Schneider, Gerardo",\neditor="Hou, Zhe\nand Ganesh, Vijay",\ntitle="Incorporating Monitors in Reactive Synthesis Without Paying the Price",\nbooktitle="Automated Technology for Verification and Analysis",\nyear="2021",\npublisher="Springer International Publishing",\naddress="Cham",\npages="337--353",\nabstract="Temporal synthesis attempts to construct reactive programs that satisfy a given declarative (LTL) formula. Practitioners have found it challenging to work exclusively with declarative specifications, and have found languages that combine modelling with declarative specifications more useful. Synthesised controllers may also need to work with pre-existing or manually constructed programs. In this paper we explore an approach that combines synthesis of declarative specifications in the presence of an existing behaviour model as a monitor, with the benefit of not having to reason about the state space of the monitor. We suggest a formal language with automata monitors as non-repeating and repeating triggers for LTL formulas. We use symbolic automata with memory as triggers, resulting in a strictly more expressive and succinct language than existing regular expression triggers. We give a compositional synthesis procedure for this language, where reasoning about the monitor state space is minimal. To show the advantages of our approach we apply it to specifications requiring counting and constraints over arbitrarily long sequence of events, where we can also see the power of parametrisation, easily handled in our approach. We provide a tool to construct controllers (in the form of symbolic automata) for our language.",\nisbn="978-3-030-88885-5",\nurl="https://gupea.ub.gu.se/bitstream/handle/2077/74140/305933.pdf"\n}\n\n
\n
\n\n\n
\n Temporal synthesis attempts to construct reactive programs that satisfy a given declarative (LTL) formula. Practitioners have found it challenging to work exclusively with declarative specifications, and have found languages that combine modelling with declarative specifications more useful. Synthesised controllers may also need to work with pre-existing or manually constructed programs. In this paper we explore an approach that combines synthesis of declarative specifications in the presence of an existing behaviour model as a monitor, with the benefit of not having to reason about the state space of the monitor. We suggest a formal language with automata monitors as non-repeating and repeating triggers for LTL formulas. We use symbolic automata with memory as triggers, resulting in a strictly more expressive and succinct language than existing regular expression triggers. We give a compositional synthesis procedure for this language, where reasoning about the monitor state space is minimal. To show the advantages of our approach we apply it to specifications requiring counting and constraints over arbitrarily long sequence of events, where we can also see the power of parametrisation, easily handled in our approach. We provide a tool to construct controllers (in the form of symbolic automata) for our language.\n
\n\n\n
\n\n\n
\n
\n\n \n \n \n \n \n Model-Based Static and Runtime Verification for Ethereum Smart Contracts.\n \n \n \n\n\n \n Azzopardi, S.; Colombo, C.; and Pace, G.\n\n\n \n\n\n\n In Hammoudi, S.; Pires, L.; and Selić, B., editor(s),
Model-Driven Engineering and Software Development, pages 323–348, Cham, 2021. Springer International Publishing\n
\n\n
\n\n
\n\n
\n\n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n \n \n abstract \n \n\n \n \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n
\n
@InProceedings{10.1007/978-3-030-67445-8_14,\n\tauthor="Azzopardi, Shaun\n\tand Colombo, Christian\n\tand Pace, Gordon",\n\teditor="Hammoudi, Slimane\n\tand Pires, Lu{\\'i}s Ferreira\n\tand Seli{\\'{c}}, Bran",\n\ttitle="Model-Based Static and Runtime Verification for Ethereum Smart Contracts",\n\tbooktitle="Model-Driven Engineering and Software Development",\n\tyear="2021",\n\tpublisher="Springer International Publishing",\n\taddress="Cham",\n\tpages="323--348",\n\tabstract="Distributed ledger technologies, e.g. blockchains, are an innovative solution to the problem of trust between different parties. Smart contracts, programs executing on these ledgers present new challenges given their non-traditional execution context -- blockchains. The immutability of smart contracts once they are deployed makes their pre-deployment correctness essential. This can be achieved through verification methods, which attempt to answer conclusively whether the code respects some specification. Another approach is model-driven development, where the specification is used directly to create a correct-by-const-ruction implementation. A specification may however still need to be verified to ensure it satisfies some properties. Verifying properties pre-deployment is ideal, however it may not always be possible to do completely, depending on the complexity of the smart contract. Traditionally upon failure of a verification attempt the only option is to attempt a different verification method. Recent approaches instead enable the transformation of the verification problem into a smaller problem, reducing the load of subsequent verification attempts. We have previously proposed an automata-theoretic approach to reason systematically about this kind of residual analysis for (co-)safety properties, while we have implemented an intraprocedural data-flow approach for Java programs. In this paper we extend our approach for Solidity smart contracts, present a corresponding tool, evaluate the approach with several new case studies, and compare it with existing approaches.",\n\tisbn="978-3-030-67445-8"\n}\n\n\n
\n
\n\n\n
\n Distributed ledger technologies, e.g. blockchains, are an innovative solution to the problem of trust between different parties. Smart contracts, programs executing on these ledgers present new challenges given their non-traditional execution context – blockchains. The immutability of smart contracts once they are deployed makes their pre-deployment correctness essential. This can be achieved through verification methods, which attempt to answer conclusively whether the code respects some specification. Another approach is model-driven development, where the specification is used directly to create a correct-by-const-ruction implementation. A specification may however still need to be verified to ensure it satisfies some properties. Verifying properties pre-deployment is ideal, however it may not always be possible to do completely, depending on the complexity of the smart contract. Traditionally upon failure of a verification attempt the only option is to attempt a different verification method. Recent approaches instead enable the transformation of the verification problem into a smaller problem, reducing the load of subsequent verification attempts. We have previously proposed an automata-theoretic approach to reason systematically about this kind of residual analysis for (co-)safety properties, while we have implemented an intraprocedural data-flow approach for Java programs. In this paper we extend our approach for Solidity smart contracts, present a corresponding tool, evaluate the approach with several new case studies, and compare it with existing approaches.\n
\n\n\n
\n\n\n
\n
\n\n \n \n \n \n \n \n Runtime Monitoring Processes Across Blockchains.\n \n \n \n \n\n\n \n Azzopardi, S.; Ellul, J.; and Pace, G. J.\n\n\n \n\n\n\n In Hojjat, H.; and Massink, M., editor(s),
Fundamentals of Software Engineering, pages 142–156, Cham, 2021. Springer International Publishing\n
\n\n
\n\n
\n\n
\n\n \n \n
Paper\n \n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n \n \n abstract \n \n\n \n \n \n 3 downloads\n \n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n
\n
@inproceedings{rvblockchains,\nauthor="Azzopardi, Shaun\nand Ellul, Joshua\nand Pace, Gordon J.",\neditor="Hojjat, Hossein\nand Massink, Mieke",\ntitle="Runtime Monitoring Processes Across Blockchains",\nbooktitle="Fundamentals of Software Engineering",\nyear="2021",\npublisher="Springer International Publishing",\naddress="Cham",\npages="142--156",\nabstract="Business processes have been long researched, with many tools, languages, and diagrammatic notations having been developed for automation. Recently, distributed ledger technology (of which Blockchain is one type) has been proposed for use in the monitoring of business process compliance. Such a set-up is attractive since it allows for immutability and thus a perfect record of the history of the business process regulated.",\nisbn="978-3-030-89247-0",\nurl = {http://www.cs.um.edu.mt/gordon.pace/Research/Papers/fsen2021.pdf}\n}\n\n\n
\n
\n\n\n
\n Business processes have been long researched, with many tools, languages, and diagrammatic notations having been developed for automation. Recently, distributed ledger technology (of which Blockchain is one type) has been proposed for use in the monitoring of business process compliance. Such a set-up is attractive since it allows for immutability and thus a perfect record of the history of the business process regulated.\n
\n\n\n
\n\n\n\n\n\n