Verification of Consistency between Process Models, Object Life Cycles, and Context-dependent Semantic Specifications
Wed 11 May 2022 03:00 - 03:05 at ICSE room 4-odd hours - Validation and Verification 2 Chair(s): Grischa Liebel
Wed 25 May 2022 11:05 - 11:10 at Ballroom A - Papers 5: Validation and Verification Chair(s): Shiva Nejati
Wed 25 May 2022 13:30 - 15:00 at Ballroom Gallery - Posters 1
Process models in general, and those specifying process-oriented software in particular, should be formally verified. While activity-oriented process models have been verified against object life cycles, formally specified semantic specifications of actions were not involved. Hence, previous approaches for the verification of process models did not make use of declaratively represented knowledge of actions. This paper presents a new approach for verification of consistency between process models, object life cycles, and context-dependent semantic action specifications. This approach involves declarative specifications of all the actions of a process, which also depend on the context of use of the actions. These context-dependent specifications define the logic of the process flow, which is grounded in (extended) object life cycles. Since a subtyping relation is enforced, reuse is facilitated through substitutability. Our extension of object life cycles makes them applicable to processes including non-monotonicity, and even to model communication based on physical interaction in cyber-physical systems. As a consequence, this formal consistency verification ensures that all the involved specifications fit together, both procedurally and logically.
Tue 10 MayDisplayed time zone: Eastern Time (US & Canada) change
12:00 - 13:00 | Validation and Verification 6Technical Track / SEIP - Software Engineering in Practice / NIER - New Ideas and Emerging Results / Journal-First Papers at ICSE room 3-even hours Chair(s): Miguel Goulao NOVA University of Lisbon | ||
12:00 5mTalk | Verification of Consistency between Process Models, Object Life Cycles, and Context-dependent Semantic Specifications Journal-First Papers Ralph Hoch Institute of Computer Technology, TU Wien, Christoph Luckeneder Vienna University of Technology, Roman Popp TU Wien, Vienna, Austria, Hermann Kaindl Institute of Computer Technology, TU Wien Link to publication DOI Pre-print Media Attached | ||
12:05 5mTalk | Evaluating Commit Message Generation: To BLEU Or Not To BLEU? NIER - New Ideas and Emerging Results Samanta Dey Chennai Mathematical Institute, Venkatesh Vinayakarao Chennai Mathematical Institute, Monika Gupta IBM Research India, Sampath Dechu IBM Research Link to publication DOI Pre-print Media Attached | ||
12:10 5mTalk | Verifying Dynamic Trait Objects in Rust SEIP - Software Engineering in Practice Alexa VanHattum Cornell University, Daniel Schwartz-Narbonne Amazon, n.n., Nathan Chong Amazon, Adrian Sampson Cornell University Pre-print Media Attached | ||
12:15 5mTalk | Verification of ORM-based Controllers by Summary Inference Technical Track Geetam Chawla Indian Insitute of Science, Bangalore, Navneet Aman Indian Institute of Science, Bangalore, Raghavan Komondoor IISc Bengaluru, Ashish Shashikant Bokil Indian Institute of Science, Bangalore, Nilesh Ramesh Kharat Indian Institute of Science, Bangalore Pre-print Media Attached | ||
12:20 5mTalk | Quantifying Permissiveness of Access Control Policies Technical Track William Eiers University of California at Santa Barbara, USA, Ganesh Sankaran University of California Santa Barbara, Albert Li University of California Santa Barbara, Emily O'Mahony University of California Santa Barbara, Benjamin Prince University of California Santa Barbara, Tevfik Bultan University of California, Santa Barbara Pre-print Media Attached |
Wed 11 MayDisplayed time zone: Eastern Time (US & Canada) change
03:00 - 04:00 | Validation and Verification 2Technical Track / Journal-First Papers at ICSE room 4-odd hours Chair(s): Grischa Liebel Reykjavik University | ||
03:00 5mTalk | Verification of Consistency between Process Models, Object Life Cycles, and Context-dependent Semantic Specifications Journal-First Papers Ralph Hoch Institute of Computer Technology, TU Wien, Christoph Luckeneder Vienna University of Technology, Roman Popp TU Wien, Vienna, Austria, Hermann Kaindl Institute of Computer Technology, TU Wien Link to publication DOI Pre-print Media Attached | ||
03:05 5mTalk | Verification of ORM-based Controllers by Summary Inference Technical Track Geetam Chawla Indian Insitute of Science, Bangalore, Navneet Aman Indian Institute of Science, Bangalore, Raghavan Komondoor IISc Bengaluru, Ashish Shashikant Bokil Indian Institute of Science, Bangalore, Nilesh Ramesh Kharat Indian Institute of Science, Bangalore Pre-print Media Attached | ||
03:10 5mTalk | Data-Driven Loop Bound Learning for Termination Analysis Technical Track DOI Pre-print Media Attached | ||
03:15 5mTalk | Refty: Refinement Types for Valid Deep Learning Models Technical Track Yanjie Gao Microsoft Research, lizhengxian Microsoft Research, Haoxiang Lin Microsoft Research, Hongyu Zhang University of Newcastle, Ming Wu Shanghai Tree-Graph Blockchain Research Institute, Mao Yang Microsoft Research DOI Pre-print Media Attached | ||
03:20 5mTalk | GraphFuzz: Library API Fuzzing with Lifetime-aware Dataflow Graphs Technical Track DOI Pre-print Media Attached | ||
03:25 5mTalk | MOREST: Model-based RESTful API Testing with Execution Feedback Technical Track Yi Liu Nanyang Technological University, Yuekang Li Nanyang Technological University, Gelei Deng Nanyang Technological University, Yang Liu Nanyang Technological University, Ruiyuan Wan Huawei Inc., Runchao Wu Huawei Inc., Dandan Ji Huawei Inc., Shiheng Xu Huawei Inc., Minli Bao Huawei Inc. Pre-print Media Attached |
Wed 25 MayDisplayed time zone: Eastern Time (US & Canada) change
11:00 - 12:30 | Papers 5: Validation and VerificationSEIP - Software Engineering in Practice / Technical Track / Journal-First Papers at Ballroom A Chair(s): Shiva Nejati University of Ottawa | ||
11:00 5mTalk | Linear-time Temporal Logic guided Greybox Fuzzing Technical Track Ruijie Meng National University of Singapore, Singapore, Zhen Dong Fudan University, China, Jialin Li National University of Singapore, Singapore, Ivan Beschastnikh University of British Columbia, Abhik Roychoudhury National University of Singapore DOI Pre-print Media Attached | ||
11:05 5mTalk | Verification of Consistency between Process Models, Object Life Cycles, and Context-dependent Semantic Specifications Journal-First Papers Ralph Hoch Institute of Computer Technology, TU Wien, Christoph Luckeneder Vienna University of Technology, Roman Popp TU Wien, Vienna, Austria, Hermann Kaindl Institute of Computer Technology, TU Wien Link to publication DOI Pre-print Media Attached | ||
11:10 5mTalk | GraphFuzz: Library API Fuzzing with Lifetime-aware Dataflow Graphs Technical Track DOI Pre-print Media Attached | ||
11:15 5mTalk | ExAIS: Executable AI Semantics Technical Track Pre-print Media Attached | ||
11:20 5mTalk | Verifying Dynamic Trait Objects in Rust SEIP - Software Engineering in Practice Alexa VanHattum Cornell University, Daniel Schwartz-Narbonne Amazon, n.n., Nathan Chong Amazon, Adrian Sampson Cornell University Pre-print Media Attached | ||
11:25 5mTalk | Quantifying Permissiveness of Access Control Policies Technical Track William Eiers University of California at Santa Barbara, USA, Ganesh Sankaran University of California Santa Barbara, Albert Li University of California Santa Barbara, Emily O'Mahony University of California Santa Barbara, Benjamin Prince University of California Santa Barbara, Tevfik Bultan University of California, Santa Barbara Pre-print Media Attached | ||
11:30 5mTalk | Fuzzing Class Specifications Technical Track Facundo Molina University of Rio Cuarto and CONICET, Argentina, Marcelo d'Amorim Federal University of Pernambuco, Nazareno Aguirre University of Rio Cuarto and CONICET, Argentina Pre-print Media Attached |