type:: [[REVIEWS]]
tags:: 
year:: 2024
venue:: [[MODELS-WS]] 
full-title:: RE-driven Model Development with Deduction-based Verification
date-start:: [[31-07-2024]] - 11:07
date-submitted::
external-links::
status:: [[DONE]] 
deadline-submission:: 
file:: [[@RE-driven Model Development with Deduction-based Verification]] 
parent::
todoist:: https://app.todoist.com/app/task/fpvm-2024-submission-assignment-6VpRg46wpmP566pg

	- ### [[Highlights]]
		- # Annotazioni
			- (1/8/2024, 16:30:30)
			- - “visualisation and pervasive approach to modelling key development artefacts, along with formal verification, may be essential in this context” ([Klimek, 2018, p. 1](zotero://select/library/items/25ZPF5JA)) ([pdf](zotero://open-pdf/library/items/B8VV4RTD?page=1&annotation=SXJY8E5S)) #5fb236
			- - “models are automatically translated into logical specifications.” ([Klimek, 2018, p. 1](zotero://select/library/items/25ZPF5JA)) ([pdf](zotero://open-pdf/library/items/B8VV4RTD?page=1&annotation=CGGZQEAD)) #ffd400
			- *Check the novelty of this!!!*
			- - “s [8]” ([Klimek, 2018, p. 1](zotero://select/library/items/25ZPF5JA)) ([pdf](zotero://open-pdf/library/items/B8VV4RTD?page=1&annotation=6HYUK9D7)) #ffd400
			- *It's a more than 10 years reference.*
			- - “valid [11]” ([Klimek, 2018, p. 1](zotero://select/library/items/25ZPF5JA)) ([pdf](zotero://open-pdf/library/items/B8VV4RTD?page=1&annotation=2EHJDBPM)) #ffd400
			- *Even worste*
			- - “Logical specifications for behavioural models are difficult to specify manually by inexperienced users, which constitutes a hindrance in the building of logic-based frameworks.” ([Klimek, 2018, p. 1](zotero://select/library/items/25ZPF5JA)) ([pdf](zotero://open-pdf/library/items/B8VV4RTD?page=1&annotation=3G3ICD7U)) #5fb236
			- - “F-IDE” ([Klimek, 2018, p. 1](zotero://select/library/items/25ZPF5JA)) ([pdf](zotero://open-pdf/library/items/B8VV4RTD?page=1&annotation=5MBKW7QP)) #5fb236
			- - “class” ([Klimek, 2018, p. 1](zotero://select/library/items/25ZPF5JA)) ([pdf](zotero://open-pdf/library/items/B8VV4RTD?page=1&annotation=QHKEQ928)) #ff6666
			- - “Our future intention is to implement a F-IDE system that will keep the analyst informed, constantly, about the inconsistency of the behaviour model regarding the planned logical assertions.” ([Klimek, 2018, p. 1](zotero://select/library/items/25ZPF5JA)) ([pdf](zotero://open-pdf/library/items/B8VV4RTD?page=1&annotation=XAGCM3BU)) #ffd400
			- *I'm not an expert but in the context of critical systems, there are already techniques and tools supporting the logical specification of systems. I remember TopCased did something similar!*
			- - “mature enough and correct” ([Klimek, 2018, p. 1](zotero://select/library/items/25ZPF5JA)) ([pdf](zotero://open-pdf/library/items/B8VV4RTD?page=1&annotation=QXCXXUQZ)) #ffd400
			- *What does it mean? Mature with respect to what?*
			- - “classic logical assertions” ([Klimek, 2018, p. 1](zotero://select/library/items/25ZPF5JA)) ([pdf](zotero://open-pdf/library/items/B8VV4RTD?page=1&annotation=ZYDKX8MZ)) #5fb236
			- - “deductive reasoning about behavioural models developed during the (in-depth) RE, and then generating program skeletons, which are equivalent to designed behavioural models” ([Klimek, 2018, p. 1](zotero://select/library/items/25ZPF5JA)) ([pdf](zotero://open-pdf/library/items/B8VV4RTD?page=1&annotation=4SIKLF4L)) #5fb236
			- - “This approach can be used in a variety of software projects to obtain formally verified and reliable skeletons for further developments” ([Klimek, 2018, p. 1](zotero://select/library/items/25ZPF5JA)) ([pdf](zotero://open-pdf/library/items/B8VV4RTD?page=1&annotation=ED5MFT2T)) #5fb236
			- - “creating graphical representations of systems and their component interactions” ([Klimek, 2018, p. 1](zotero://select/library/items/25ZPF5JA)) ([pdf](zotero://open-pdf/library/items/B8VV4RTD?page=1&annotation=IHT2A5RQ)) #5fb236
			- - “Consequently, visual models enhance the comprehension of complex systems and improve project management efficiency” ([Klimek, 2018, p. 1](zotero://select/library/items/25ZPF5JA)) ([pdf](zotero://open-pdf/library/items/B8VV4RTD?page=1&annotation=MAQP396U)) #a28ae5
			- - “Correctness-by-Construction” ([Klimek, 2018, p. 1](zotero://select/library/items/25ZPF5JA)) ([pdf](zotero://open-pdf/library/items/B8VV4RTD?page=1&annotation=N8J8WKMI)) #5fb236
			- - “compositional approach,” ([Klimek, 2018, p. 2](zotero://select/library/items/25ZPF5JA)) ([pdf](zotero://open-pdf/library/items/B8VV4RTD?page=2&annotation=3B28YLXY)) #5fb236
			- - “Requirements eLicitation (RL)” ([Klimek, 2018, p. 2](zotero://select/library/items/25ZPF5JA)) ([pdf](zotero://open-pdf/library/items/B8VV4RTD?page=2&annotation=7VAQPQYT)) #a28ae5
			- - “Requirements Analysis (RA)” ([Klimek, 2018, p. 2](zotero://select/library/items/25ZPF5JA)) ([pdf](zotero://open-pdf/library/items/B8VV4RTD?page=2&annotation=T4DES9H4)) #a28ae5
			- - “Requirements Specification (RS)” ([Klimek, 2018, p. 2](zotero://select/library/items/25ZPF5JA)) ([pdf](zotero://open-pdf/library/items/B8VV4RTD?page=2&annotation=SANSQS92)) #a28ae5
			- - “Requirements Verification (RV)” ([Klimek, 2018, p. 2](zotero://select/library/items/25ZPF5JA)) ([pdf](zotero://open-pdf/library/items/B8VV4RTD?page=2&annotation=QGZAGB9K)) #a28ae5
			- - “A more precise description of the RV phase and its steps is given below” ([Klimek, 2018, p. 2](zotero://select/library/items/25ZPF5JA)) ([pdf](zotero://open-pdf/library/items/B8VV4RTD?page=2&annotation=5R7LIQQ5)) #5fb236
			- - “deduction theorem” ([Klimek, 2018, p. 2](zotero://select/library/items/25ZPF5JA)) ([pdf](zotero://open-pdf/library/items/B8VV4RTD?page=2&annotation=8VU5R2RJ)) #5fb236
			- - “Remark 1. The presented structuring demonstrates a natural progression from general artifacts to increasingly formal behavioural models, which undergo rigorous logical verification.” ([Klimek, 2018, p. 2](zotero://select/library/items/25ZPF5JA)) ([pdf](zotero://open-pdf/library/items/B8VV4RTD?page=2&annotation=TPBUDWTX)) #a28ae5
			- - “A set of patterns” ([Klimek, 2018, p. 3](zotero://select/library/items/25ZPF5JA)) ([pdf](zotero://open-pdf/library/items/B8VV4RTD?page=3&annotation=3AFAS4WT)) #5fb236
			- - “Π = {Seq, SeqSeq, Cond, Alt, Para, Loop}” ([Klimek, 2018, p. 3](zotero://select/library/items/25ZPF5JA)) ([pdf](zotero://open-pdf/library/items/B8VV4RTD?page=3&annotation=ID3YP4VD)) #5fb236
			- - “Compositionality in workflows” ([Klimek, 2018, p. 3](zotero://select/library/items/25ZPF5JA)) ([pdf](zotero://open-pdf/library/items/B8VV4RTD?page=3&annotation=GMAHZF8Q)) #5fb236
			- - “Propositional linear-time temporal logic PLTL” ([Klimek, 2018, p. 3](zotero://select/library/items/25ZPF5JA)) ([pdf](zotero://open-pdf/library/items/B8VV4RTD?page=3&annotation=PCRSSMCE)) #5fb236
			- - “They are used in a process of translating the natural language of scenarios into formal activity diagrams AD j=1,... as workflows.” ([Klimek, 2018, p. 3](zotero://select/library/items/25ZPF5JA)) ([pdf](zotero://open-pdf/library/items/B8VV4RTD?page=3&annotation=WL8SLYZX)) #ffd400
			- - “Figure 3: The basic system architecture of LoRE+, and its data flows. (Modellers, builder and creator provide the possibility of interactive work when developing a software system, while generator and reasoner guarantee fully automatic verification operations. The Gen generator implements two algorithms, see Formulas (2) and (3). Π and Σ are defined once and used widely)” ([Klimek, 2018, p. 4](zotero://select/library/items/25ZPF5JA)) ([pdf](zotero://open-pdf/library/items/B8VV4RTD?page=4&annotation=FXJDPMRL)) #ffd400
			- *It's difficult to see how the process can work in practice. Starting from textual specifications, logical formulas are generated. Such a critical process is vaguosly presented and the conditions under which this can work are not discussed.*
			- - “available upon request” ([Klimek, 2018, p. 4](zotero://select/library/items/25ZPF5JA)) ([pdf](zotero://open-pdf/library/items/B8VV4RTD?page=4&annotation=6JB9LISD)) #ffd400
			- *Why not making this available directly?*
			- - “This problem involved investigating how the size of a formula affects testing time, assuming the formula comprises groups of clauses with fixed lengths (number of used variables/atoms/literals). We generated formulas consisting of 50, 100, 200, 500, 1000, and 2000 clauses separately.” ([Klimek, 2018, p. 4](zotero://select/library/items/25ZPF5JA)) ([pdf](zotero://open-pdf/library/items/B8VV4RTD?page=4&annotation=55DGFUZJ)) #ffd400
			- *All of this are vaguos and are not conveying any message. Instead, the authors are invited to revise the paper by discussing an running example to show how the different components of the proposed approach work in practice. By discussing them in this manner, it is possible to highlight the strenghts and the limitations of the proposed approach with respect to the state-of-art techniques.*
			- - “Figure 4: Problem #5 for Prover9 (top), SPASS (middle) and InKreSAT (bottom), clauses against time” ([Klimek, 2018, p. 4](zotero://select/library/items/25ZPF5JA)) ([pdf](zotero://open-pdf/library/items/B8VV4RTD?page=4&annotation=ZZ7HGB59)) #ffd400
			- *It's not possible to appreciate the strenghts of the approach and the data shown in Fig. 4 without properly presenting the context where they have been produced, etc.*
	- ### [[Comments]]
		- SUMMARY: The paper presents a framework named LoRE+ that integrates requirements engineering (RE) with formal verification through a deductive approach. The approach supports the generation of program skeletons from source models and offers a methodology that claims to ensure correctness and consistency through deductive reasoning.
		- COMMENTS: Even though the paper is about a relevant topic, I have several concerns about the work that are related to the following issues:
			- While the proposed methodology in LoRE+ aims to bridge RE and formal verification, the novelty appears limited in comparison to existing frameworks. The concept of translating models into logical specifications and ensuring correctness through formal methods is not new. For instance, frameworks and tools like Polarsys have already explored similar domains. The paper must more clearly differentiate its approach from these existing works, especially considering the decade-old references cited. The paper is also missing related work like Autili et. al. on "Graphical scenarios for specifying temporal properties: an automated approach" https://link.springer.com/article/10.1007/s10515-007-0012-6
			- The description of the transformation from textual specifications to logical formulas needs to be more specific. The paper introduces the concept of generating logical specifications from activity diagrams but needs to discuss the conditions under which this process is effective. The lack of detailed examples and practical applications weakens the presentation of the methodology.
			- The paper acknowledges the limitations of manual specification of logical requirements, particularly for inexperienced users. However, the critique of existing techniques is superficial. For instance, the assertion that the approach is "mature enough and correct" is ambiguous without a clear benchmark or comparison. The discussion should be grounded in more concrete terms, e.g., by evaluating the framework against specific criteria or using established benchmarks in the field.
			- The emphasis on visualization to improve understanding and management of complex systems is well-founded. However, the paper could benefit from a more detailed discussion of how these visualizations contribute to the overall process. It would be useful to compare the effectiveness of these visual models with traditional methods.
			- The evaluation section is insufficient. I know this is a workshop paper, but the manuscript provides high-level discussions without substantial empirical evidence. The paper would greatly benefit from including (even simple) case studies or experimental data that illustrate the practical applicability and limitations of the LoRE+ framework.
	- ### [[REVIEWS/Notes]]
	- ### YELLOW CONCERNS
	  background-color:: yellow
		- {{query (and [[ffd400]] [[FPVM2024_paper_5]] )}}
		  collapsed:: true
	- ### ❓️Questions
		- {{query (and [[question]] [[FPVM2024_paper_5]] )[[question]]}}
		  query-table:: true
		  query-properties:: [:block]