08-Formalization.pdf

Requirements Engineering Lecture 8 Prof. Dr. Alexander Pretschner Chair of Software & Systems Engineering TUM School of CIT Technical University of Munich Orientation Recap:...

Requirements Engineering Lecture 8 Prof. Dr. Alexander Pretschner Chair of Software & Systems Engineering TUM School of CIT Technical University of Munich Orientation Recap: Lecture 7: Functional Requirements Use Cases, Function Hierarchies Coming up: Formalization: How to formalize Functional Requirements? Application in the context of a model-based RE Tradeoff: Precision vs. Comprehensibility Tradeoff: Precision vs. Intentional Imprecision Requirements for Machine Learning Requirements Engineering | SS 2024 | TUM i4 4 Precision of Requirements Specifications Requirements in user stories are rather informal and possibly imprecise Requirements in use case descriptions may be more precise When do we need precision of requirements? User requirements? System requirements? How can we achieve it? By formalization using … metrics … formulas … models with a formal semantics. (When) Is this helpful? Requirements Engineering | SS 2024 | TUM i4 5 Discussion: Quality Metrics Can one set of quality metrics work for all kinds of software? Requirements Engineering | SS 2024 | TUM i4 6 Interpretation of Statements on Properties Statements on requirements serve: the professional communication between project participants the documentation for analysis by - People - Machines Natural language is used for communication between people. Essential prerequisites for Natural Languages are: Uniform understanding (same interpretation) Knowledge of the language or technical language Requirements Engineering | SS 2024 | TUM i4 8 Exemplary Statements on Requirements The system should respond as soon as possible. Operating errors are largely excluded. Remem The system is self-explanatory. Quality c ber: riteria fo The system is highly reliable. r require men ts! All processes in the system are traceable. The system is inexpensive. Requirements Engineering | SS 2024 | TUM i4 9 Problems: Precision and Explicitness The system should respond as soon as possible. Operating errors are largely excluded. Remem The system is self-explanatory. Quality c ber: riteria fo The system is highly reliable. r require men ts! All processes in the system are traceable. The system is inexpensive. Interpretation of the statements meaning: Unambiguous: meaning independent of individual interpretation Comprehensible: target group can recognize and understand the meaning Precision: Clear identification of a system property Verifiable: For a system it can be observed / measured whether the formulated property is fulfilled Requirements Engineering | SS 2024 | TUM i4 10 A Note on Ambiguity Requirements Engineering | SS 2024 | TUM i4 11 Formalization - What is that? Definition Formalization: Formulation and Representation of content in a form independent of individual (subjective) interpretation and based on a given system of definitions (theory) How to apply Formalization: Formal Language Semantics − Translation into reference systematics (logic, mathematics) − Rules for the transformation and deduction of further contents ("statements") Metrics → Typically, proven and prepared formalization concepts are used for formalization. Requirements Engineering | SS 2024 | TUM i4 12 Examples for Formalization Concepts Data modelling − Ontologies − Taxonomies Logic − Predicate Logic − Temporal Logic State Machines Interfaces Architectures Metrics Requirements Engineering | SS 2024 | TUM i4 13 Formalization provides Precision Natural Language: ambiguous, contextual (example: “Band") very complex → Informally described requirements are usually not precise and thus not free of subjective interpretation (Hence, they are ambiguous) Formalization provides a more precise definition Formalization clearly defines the meaning, i.e., one interpretation of the requirement, which is at first only formulated in natural language, is chosen from a set of possible interpretations (Requires validation: Is this specification the desired one? OUCH!) Choice of certain formalization concepts: This raises the question of comprehensibility and manageability. → Precise requirements can be better validated and analyzed. However: Specification of system properties requires a precise definition of “system", or even a formal model for a System. And it requires precisely understood requirements! Requirements Engineering | SS 2024 | TUM i4 14 But once again: Do we really want this? Formalization means precision, possibly unintended precision (e.g., vacuity claims) Are requirements precise? Um. ChatGPT? Requirements Engineering | SS 2024 | TUM i4 15 Discussion: Traffic Light State Machine A traffic light state machine is in the state “cyclic mode”, where it cycles between the 4 sub-states symbolizing the different lights. After 10 pm, the traffic light switches to the state “blinking”. At 6 am, it switches back to “cyclic mode”. In what sub-state is it now? Requirements Engineering | SS 2024 | TUM i4 16 Formalization and Quality Requirements of IEEE 830 Correct: better "valid", formulated vs. actual requirements (stakeholder expectations), requires precision Unambiguous: Formalization can help if it is understandable Complete: Formalization can help to uncover incompleteness Consistent: Consistency - formal logic consistency Verifiable: In mathematical sense only with formalization Modifiable: Change effects through formalization of visible Traceable: Formalization simplifies requirement relationships Ranked for Importance/Stability: Does not affect formalization Requirements Engineering | SS 2024 | TUM i4 17 Formulation of Statements Subjectivity: Related to the communication partners ("subjects") – Ability to formulate given statements precisely (for the producer) and to understand them (for the consumer) Objectivity: Related to a description system – Statements reduce subjectivity through methods of description (formalization) that are independent of subjective judgements – Attention: Objectivity leads to the problem of subjectivity by asking whether producers and consumers are capable of formulating and understanding in the description system. Intersubjectivity: An issue is equally recognizable and comprehensible for several viewers – There is agreement on how to perceive the facts, how to classify them and what they mean. Requirements Engineering | SS 2024 | TUM i4 18 One Tradeoff: Precision vs. Comprehensibility vs. Precision ("objective"): Comprehensibility ("subjective"): How precise are Requirements How good and simple are formulated requirements to understand → Ultimately requires formalization → Depending on target group Caveat: A very precisely formulated requirement can be difficult to understand (e.g., if the formalism used is not familiar to the target group)! A requirement can be misinterpreted or not understood. A requirement that is (apparently) very understandable from an individual point of view can be interpreted in different ways. → It can be misinterpreted and thus misunderstood. Requirements Engineering | SS 2024 | TUM i4 19 Empirically Formulated Statements on Properties Statements about the properties of systems can also be formulated empirically: → Capturing the statements by observations of systems and their environment. → Verification by experiments and measurements possible. → Metrics! Examples: A system error occurs only once in 10 hours for a given operating situation. With 10 entries from a certain sample 9 usable answers are generated. Difficulties / Problems: Falsification of the properties by further refuting observations is always possible (except for static metrics, e.g., McCabe) Requirements Engineering | SS 2024 | TUM i4 20 Conclusion: Statements on Properties Formulation of Statements on Properties: Subjective: No explicit model/description system Objective: Explicit model/description system Empirical: No mathematical prediction/explanatory model – Observations/Measurements Formalized: Mathematical prediction/explanatory model Partially Combinable Connection: Statement about property used as a requirement for a system to be built Formalized requirements and agility? Requirements Engineering | SS 2024 | TUM i4 21 Formulation of Statements Informal: Syntax and Semantics not formally defined Example: Natural language, sketches, informal diagrams, etc. Semi-formal: Syntax formally defined Example: UML, SysML, Matlab Simulink Formal: Syntax and Semantics formally defined Example: Propositional and predicate logic, temporal logic, Petri nets, 𝜆-calculus, programming languages Note: "Semantics" is a mapping of mathematical objects into other mathematical objects that seem to be more intuitively understandable Requirements Engineering | SS 2024 | TUM i4 22 The Term "Model" (Repetition) What is a Model? Attention: Models are usually bound to a purpose, shortened images of a mental or real, existing or future reality. Models do not have to have a formal basis (i.e., defined with mathematical and computer tools), even if they are documented in a formally defined notation. → Both their meaning and their representation can also be handled informally. Requirements Engineering | SS 2024 | TUM i4 23 System Models Definition System Model: A system model is a meta model which defines an abstract syntax. This abstract syntax is usually specified in a modeling tool. A system model describes certain model viewpoints of a system, which determine the structure or the behavior of this system and their relations among each other. Definition Views: Views show a system from a certain perspective (viewpoint). They offer suitable modeling concepts for these perspectives and thus enable a precise observation and analysis of these perspectives. A view is an instance of a viewpoint. System Models determine what requirements are talking about: What is a system? What are the essential characteristics, views and structures? Which components and structures does a system have? Requirements Engineering | SS 2024 | TUM i4 24 Difference between System Models and Models of a System ≠ System Model (“meta model"): Model of a System (“artifact model"): Which constructs are necessary to Ideally built on system models like describe models. Conceptual model content models. Structuring of models using different viewpoints on a in structure models. system. → Artefact model like e.g., BPMN, → System is modeled in two State Chart Diagram, Use Cases consistent views e.g., class diagram and sequence diagram Requirements Engineering | SS 2024 | TUM i4 25 Examples for System Models Wide range of system models and modeling languages available and used in practice: Software: Programming models like UML (UML is a set of coupled and consistent meta models) Embedded: Control engineering like MATLAB-Simulink models Example System Model: There are two view types defined in a meta model like a sequence diagram and class diagram Each actor in the sequence diagram represents an instance of a class in a class diagram If a name of an actor (which is present as a class in the class diagram) is missing in the sequence diagram, then inconsistency is present in the model Syntactic inconsistency needs to be avoided with system models. (What distinguishes syntax from semantics?) Requirements Engineering | SS 2024 | TUM i4 26 What is a System? Definition System: A system is delimited from its environment (operational context) by defining its system boundary. A system has an interface that defines (1) which forms of interaction between a system and its environment are possible (static/syntactic interface) and (2) which behavior the system shows from the context view (interface behavior, dynamic interface, interaction view). A system has an architecture. The architecture consists of elements (components, subsystems) that are interrelated. System limit / Interface to the Architecture/ environment Subsystems System System Environment Environment Requirements Engineering | SS 2024 | TUM i4 27 Projective vs. Synthetic Models Requirements Engineering | SS 2024 | TUM i4 28 Projective vs. Synthetic vs. Projective (“god model"): Synthetic (“coupling of models"): Holds all models for all views. God Different views or view types models gets projected into implemented with specific tools are requested views. pairwise coupled. → Consistency is given “for free” → worst case quadratic couplings Is the effort (cost, maintenance, collaboration) justifiable for the benefits (higher quality) that those models promise? → Probably not for software → But probably for hardware Requirements Engineering | SS 2024 | TUM i4 29 Critical Aspects when using Models Effort/Benefit when using models (e.g., detailed scenarios for "trivial" issues; synchronization!) Complexity of models and choice of notation Analysis and documentation of scenarios is crucial: → Scenarios form a communication bridge between - Stakeholders (for analysis/coordination) - Architects (draft) - Testers (specification of test cases) → Trade-Off: The more precise/formal the modeling, the more targeted questions can be asked and be handled by the stakeholders - but the more you (have to) define! → Explicit feedback to stakeholders, their goals and requirements → Exposure of need for clarification, conflicts → Vote, negotiate, prioritize and decide Requirements Engineering | SS 2024 | TUM i4 30 Formalization versus Modeling Formalization Requires: Models Require: A formal description language Implicit model building and is therefore – A set of description/modeling concepts – An abstraction – Based on a specific system view – Only as correct as observations of reality correspond to those on the model (validity of a model) Falsification of a model: Through observation, contradictions between model and reality are detected. And sure: a language for modeling Requirements Engineering | SS 2024 | TUM i4 31 Model versus Reality A (formal) model is always an abstraction of reality → Formalization and modeling create an independent view of systems → Formalization only allows the formulation of certain properties that can be spoken about in the model. But: Systems (even Software!) are ultimately part of our reality → Note difference between model and reality (Danger of detachment from reality) → Always consider to what extent the model validly represents a property of the system. → Precision is sometimes unintentional and invalid! Requirements Engineering | SS 2024 | TUM i4 32 Discussion: Informal Models Which types of model are not formalized? Are models already some form of formalization? Requirements Engineering | SS 2024 | TUM i4 33 System Specification Context Layer Project Scope ! Constraints & Rules Business Case ! ! ! ! Relevant results for the system specification of the RE are: Stakeholder Model Objectives & Goals Domain Model Context model: description of the operating environment Glossary (neighboring systems, physical/technical environment, users) Requirements Layer Data model System Vision Interface description Usage Model Service Model Process Requirements – Syntactic interface (based on the data model) Deployment Requirements – Functionality (structured as function hierarchy) Functional Hierarchy A E Data Model A Risk List – Interface behavior of the individual functions E A System Constraints Quality Requirements Glossary § as state machine § as interface assurances System Layer Architecture Overview Function Model Data Model Fun 1 A A E System Fun 2 E A Component Model Behaviour Model Glossary C C Requirements Engineering | SS 2024 | TUM i4 34 System Viewpoints States: Which states/transitions are there? Sequence/Interaction: What message/interaction sequences can there be? Data: What messages do the components exchange? Interfaces: Which messages go through which ports? Distribution: Which components are connected and how? Different formalisms exist for all views. (See for example “formal lectures”) Requirements Engineering | SS 2024 | TUM i4 35 State Machines (SM) with Inputs and Outputs Definition State Machine (SM): A nondeterministic finite SM (Δ, Σ! ) with input alphabet 𝐼 and output alphabet 𝑂 consists of a set of states Σ, initial states Σ! ⊆ Σ (or one initial state 𝜎! ∈ Σ) and a state transition function Δ: Σ×𝐼 → ℘(Σ×𝑂) Such SMs are also called Mealy Machines 𝑄 𝑖 / 𝑜 {𝑅} – Output depends on input and state Special case Moore Machine 𝑘 𝑘! – Output depends only on the state Notation for transitions in diagrams Requirements Engineering | SS 2024 | TUM i4 36 From Requirements to State Machines (SM) Functional Requirement: A user needs to log into the App. After successfully logging in they can reserve a Scooter or directly start a rent. The reservation is limited to 15min and the user would need to reserve again after that time. If the user has an active reservation, they can also start the rent for that Scooter. Example of an FSM that formalizes the mentioned requirement: input password end rent log out start rent logged- logged- rent out in active (cancel reservation) ∨ (15min reservation limit) reservation start rent failed authentication reserve scooter active Requirements Engineering | SS 2024 | TUM i4 37 Mathematical Logic Formal Syntax: Definition of the statement formulation – Textual, graphical (formal languages, metamodels) Formal Semantics/Significance: Model Theory – Definition of a universe – Determines the interpretation of formulas: Validity Formal Derivative Theory: Calculations – Rules for transforming formulas: Derivation rules → Correctness: create only "true" formulas from "true" formulas – Concept of derivation (proof): Derivation trees Important Terms: Correctness: What is derivable is valid Completeness: What is valid can be derived Consistency/non-contradiction Requirements Engineering | SS 2024 | TUM i4 38 Discussion: Syntax and Semantics What is the difference between Syntax and Semantics? Requirements Engineering | SS 2024 | TUM i4 39 Example: Behavioral Requirements Using Logic Informal (natural language): If no target vehicle exists, the ACC switches to the state in which the vehicle speed eventually is equal to the set target speed. Semi-formal (controlled grammar): IF "Target vehicle is not detected" THEN "ACC in constant speed control state" AND "ACC" MUST "Adjust vehicle speed to set target speed” Formal (temporal logic): G(target_vehicle_not_exists → ¢ (acc_const_speed_control) ∧ ◊(ego_vehicle_speed = target_speed)) Requirements Engineering | SS 2024 | TUM i4 40 Motivation: Temporal Properties If a user has reserved a scooter and starts the rent in the next timestep, the rent will eventually end in some future timestep Temporal Logic is used to make statements about state-based systems: Statements about states Statements about executions Requirements Engineering | SS 2024 | TUM i4 41 Linear Time Temporal Logic (LTL) Streams of states are sequentially ordered. Properties of streams can be described with predicates. Linear Time Temporal Logic (LTL) is a special method for formulating predicates over infinite state streams. “next P” P “eventually P” P “always P” P P P P P “P until Q” P P P Q Q Requirements Engineering | SS 2024 | TUM i4 42 Concept: Next-Operator Goal: Description of at the next time step valid properties Concept: Next-Property Notation: (“Next P”) Interpretation: Property P is valid at the next time step, P is valid in the next state. “next P” P Example: “The ACC constant speed control is activated in the next time step” Requirements Engineering | SS 2024 | TUM i4 43 Concept: Eventually-Operator Goal: Description of in the future valid properties Concept: Eventually-Property Notation: (“Eventually P”, “Finally P”) Interpretation: At one point in time after the current point Property P is valid, P is valid somewhere on the “eventually P” subsequent path. P Example: “The ego vehicle speed will become the selected target speed at a future time” Requirements Engineering | SS 2024 | TUM i4 44 Concept: Always-Operator Goal: Description of always valid properties Concept: Always-Property Notation: (“Always P”, “Globally P”) Interpretation: From now on, P is always valid. “always P” Example: “When a user has started a scooter rental, the P P P P P rental always has to end.” Requirements Engineering | SS 2024 | TUM i4 45 Concept: Until-Operator Goal: Binary Operator that describes relations between two properties followed by each other Concept: Until-Property Notation: (“P until Q”) Interpretation: P has to hold at least until Q becomes “P until Q” true. P P P Q Q Example: “If a user fails to authenticate, he is in the state “logged-out” until he correctly inputs his password and gets into the state “logged-in” Requirements Engineering | SS 2024 | TUM i4 46 Discussion: Linear Time Temporal Logic (LTL) Use LTL to describe: “Whenever the emergency brake is activated, the scooter will stop at some future point” Requirements Engineering | SS 2024 | TUM i4 47 Discussion: Eventuality Operator What other properties are typically described with the unbounded eventuality (◊) operator? Requirements Engineering | SS 2024 | TUM i4 48 Discussion: Why do all this? Why would we want to formalize requirements at all? When would we want to formalize them in this way? Requirements Engineering | SS 2024 | TUM i4 49 Forms of Formalized Requirements using Logic General predicate logic without reference to general system modeling concepts: – Example: Crash ⇒ Airbag Rudimentary system terms (time, space, sequence) – Example of temporal logic: The following always applies: A crash leads to the airbag being triggered (at some point in the future). Formulated system model (system boundary, interface behavior) – Example: Be crash_sensor_out and airbag_activation_in channels and be the statement m:c@t±s the statement message m on channel c at time t (if s ≠ in interval [t-s, t+s]) measured in msec. crash_signal:crash_sensor_out@t ⇒ act_airbag_Signal:airbag_activation_int@t+160±20 Requirements Engineering | SS 2024 | TUM i4 50 Specification Templates (According to set Patterns) Property Patterns Occurrence Order Absence Universality Existence Bounded Precedence Response Chain Chain Existence Precedence Response Dwyer et al. state: Most of the specifications correspond to the following categories: Existence: Certain event must occur at least once Absence: Certain event must not occur Precedence: Event Y comes after event X Response: Event Y is the response to event X Requirements Engineering | SS 2024 | TUM i4 51 Alternatives for Templates Formula Templates (e.g., after Dwyer et al.), controlled vocabulary and grammar Specification Templates Message Sequence Charts (MSC), Finite-state UML Sequence Diagrams (Caution!) Machines Requirements Engineering | SS 2024 | TUM i4 52 Specification Pattern "if..., then..." Template: If A, then B - discussion as regular expressions Is the sequence (A+)B allowed? Is the sequence AB+ allowed? Is B allowed without A? Is A required for B: Is the sequence A*B allowed? Is the sequence BAB allowed? Does a second A have to be followed by a second B? Requirements Engineering | SS 2024 | TUM i4 53 Further Specification Templates as Message Sequence Charts Which processes are allowed? action action action action response X,Y response response response response action action response response response action Requirements Engineering | SS 2024 | TUM i4 54 Advantages and Disadvantages of Formalization Pro/Strengths: Contra/Weaknesses: Precise, clear description Limited expressiveness Automation – Abstraction bound to a purpose – Model testing Poor intelligibility – Test case generation – Fear of contact – Program generation If unnecessary unintended precision Clear terms for High initial outlay – Consistency – Costs for training – Completeness – Experience Rules for derivation Modification may be difficult Traceability Poor scalability Verifiability with formal proof Requirements Engineering | SS 2024 | TUM i4 55 Discussion: System Formalization Given the “Juicer” subsystem of the scooter App, where a person collects several out of charge scooters, brings them to a charging station, and redistributes charged scooters on positions calculated by the app, would you formalize this system? Which kind of formalization would you choose? Requirements Engineering | SS 2024 | TUM i4 56 Requirements for Machine Learning Definition Machine Learning (ML): Machine Learning (ML) generates outputs based on statistical correlations to training data. The input-output pairs of a ML System are thus not specifically programmed but learned through sample data. Machine Learning: Used in different applications like computer vision, speech recognition, medical diagnosis Different ML algorithms exist such as SVM, Decision Trees, Linear Regression, Bayesian Networks, Genetic Algorithms, Neural Networks, Deep Learning Learning through optimization: Different training algorithms like evolutionary algorithms, gradient descent, information gain, expectation–maximization Problem: How to define Functional and Non-Functional Requirements for ML Systems? Requirements Engineering | SS 2024 | TUM i4 57 Repetition: Problem and Solution Machine Learning is the solution, not the problem Requirements for ML Systems are hard to specify: Functional Requirement Example: “Detect all pedestrians in the image” If we could formally (rule based) specify the output of an ML system, why would we need a ML system in the first place? (one reason: performance!) What is the contradiction between the usage of ML and the demand of precise and unambiguous system requirements? → Problems for which Machine Learning is adequate usually have no formal and exact specification → Exception: heuristic solutions where exact solutions are expensive Requirements Engineering | SS 2024 | TUM i4 58 Non-Functional Requirements for Machine Learning Different types of non-functional requirements for ML exist: Fairness Transparency / Explainability Privacy Security Other qualities of ML models: Correctness/Performance: Metrics like Precision, Recall, Average Precision, Intersection over Union Computational Efficiency; energy: Is the model lightweight or do we need a GPU server to run inference? Interpretability: How does the model work? Why did the model come to that conclusion? Robustness: Is the model prone to attacks and does it work in new/unusual environments? Requirements Engineering | SS 2024 | TUM i4 59 Performance Requirements for Machine Learning How can we show that a specific functional requirement is fulfilled? Test for performance metrics (90% accuracy) Test on the collected dataset might be problematic Need to avoid overfitting on training data with validation techniques (validation set, cross validation) How can we show that a specific non-functional requirement is fulfilled? For instance, runtime performance in Deep Learning influenced by model size (trade off between requirements → slow response means high accuracy) Training != Using Requirements Engineering | SS 2024 | TUM i4 60 Fairness Requirements for Machine Learning As ML decisions are often difficult to understand fairness is a recently emerging non-functional Requirement: Fairness Through Unawareness: An Algorithm is fair if it doesn’t use "protected attributes" for decision making. (Delete protected attributes from train/test datasets. Correlations?) Counter-Factual Fairness: A ML model is fair if the output remains the same if the protected attribute is flipped to a counter-factual value Individual Fairness: A ML model should give similar predictions among similar individuals according to some distance measure. Some sensitive features in the data are also present through Proxies and fairness cannot be ensured just by not using sensitive features. (e.g., the race of a person might correlate to the neighborhood it lives in) Requirements Engineering | SS 2024 | TUM i4 61 Performance Metrics for ML models Example Binary Classification: A binary classifier is trained to predict whether an item is class A or class B. Therefore, it predicts for each item a value between 0 and 1. By choosing different threshold values (e.g., 𝛽 = 0.3 or 𝛽 = 0.4) the output of the classifier can be altered. A classifiers performance for a certain 𝛽 can be described with a confusion matrix: True Class !" True Positive Rate: 𝑇𝑃𝑅 = !"#$% Class A Class B Predicted True False $" False Positive Rate: 𝐹𝑃𝑅 = $"#!" Predicted Class A Positive Positive Class Predicted False True Accuracy: !"#!% 𝐴𝐶𝐶 = !"#!%#$"#$% Class B Negative Negative Requirements Engineering | SS 2024 | TUM i4 62 Performance Metrics for ML models With changing the classification threshold 𝛽 we can adjust the trade of between the true positive rate and the false positive rate of our model. For obtaining a general metric, independent of the AUC = 0.903 classifiers setting 𝛽, of “how good” the model is, we measure the model's performance for many 𝛽 values. For each setting we note 𝑇𝑃𝑅 and 𝐹𝑃𝑅 values and plot them in a graph. The area under the curve (AUC) of this graph is a more general ML performance metric. Similarly, one can plot Precision and Recall values. Requirements Engineering | SS 2024 | TUM i4 63 Formulating Machine Learning Requirements Clear Separation of Problem and Solution: Should we specify requirements differently just because it is for ML? High level natural language requirements work for ML Detailed, specific rule-based requirements usually not possible for ML Detailed requirements over input, output pairs possible (data set) Determine acceptable measures related to the confusion matrix, or robustness measures, before the model is trained → Having this Separation of Problem and Solution would be good → However, this doesn’t always work Requirements Engineering | SS 2024 | TUM i4 64 Summary Formalization in model-based RE supported: Precise formulation and interpretation of statements on required system properties Clear terminology and Traceability Possibilities for automation Verifiability with formal proof However, the following applies to formalization Necessity of an underlying system model and associated with it possibly a limited expressiveness High effort for creation and modification of formal models Trade-off between costs and benefits necessary! Problems for which Machine Learning is adequate often don’t have a specification Requirements Engineering | SS 2024 | TUM i4 65 Outline and Outlook Terms and Definitions Context-specific nature of SE and RE Quality models for requirements Engineering Models Stakeholder and Requirements Elicitation Goals and Goal-oriented RE Non-functional Requirements Functional Requirements Formalization Agile Processes Requirements Management and Quality Assurance Trends in Research Requirements Engineering | SS 2024 | TUM i4 66