Quartz sync: Sep 19, 2023, 7:37 PM
This commit is contained in:
parent
1bf7e3d8b3
commit
d676a6a37e
SSH key fingerprint:
SHA256:JiuxZNdA5bRWXPMUJChI0AQ75yC+cXY4xM0IaVwEVys
10 changed files with 424 additions and 1 deletions
BIN
bun.lockb
Executable file
BIN
bun.lockb
Executable file
Binary file not shown.
7
content/CP/T - Aula 2 - 19 Setembro.md
Normal file
7
content/CP/T - Aula 2 - 19 Setembro.md
Normal file
|
|
@ -0,0 +1,7 @@
|
|||
## Conteúdo
|
||||
- cache em arquiteturas multicore
|
||||
- code profiling
|
||||
- instruction-level paralelism
|
||||
- Data dependency
|
||||
- branch prediction
|
||||
-
|
||||
37
content/MFES/MFES - UC Details.md
Normal file
37
content/MFES/MFES - UC Details.md
Normal file
|
|
@ -0,0 +1,37 @@
|
|||
## Programa
|
||||
|
||||
1. Lógicas para especificação formal
|
||||
1. [[T - Aula 2 - 18 Setembro 2023#Proposicional Logic (PL)| Lógica Proposicional (PL)]]
|
||||
2. Lógica de Primeira Ordem (FOL)
|
||||
3. Lógica relacional (RL)
|
||||
4. Lógica temporal linear (LTL)
|
||||
2. Técnicas de prova automática
|
||||
1. SAT solving para lógica proposicional
|
||||
2. SMT solving para lógica e teorias de primeira ordem
|
||||
3. Model-finding via SAT para lógica relacional
|
||||
4. Bounded model-checking via SAT para lógica temporal
|
||||
3. Concepção formal de software com Alloy
|
||||
1. Modelação estrutural
|
||||
2. Modelação comportamental
|
||||
4. Especificação e verificação de programas com Why3
|
||||
1. Linguagem lógica, teorias (biblioteca) e prova
|
||||
2. Linguagem de programas, especificação comportamental, e verificação de correção
|
||||
3. Desenvolvimento de sistemas com estado
|
||||
|
||||
## Docentes
|
||||
- Maria João Frade - [mjf@di.uminho.pt](mailto:mjf@di.uminho.pt)
|
||||
- Alcino Cunha - [alcino@di.uminho.pt](mailto:alcino@di.uminho.pt)
|
||||
- Jorge Sousa Pinto - [jsp@di.uminho.pt](mailto:jsp@di.uminho.pt)
|
||||
|
||||
## Avaliação
|
||||
- 20% - Exercícios de avaliação
|
||||
- 80% - Teste individual
|
||||
|
||||
Nota: As notas acima de 18 valores (quer na avaliação contínua quer no exame) terão que ser defendidas através da realização de um pequeno projecto.
|
||||
|
||||
|
||||
## Planificação
|
||||
- 6 Outubro - Entrega do 1º exercício de avaliação. Modelação em PL e FOL.
|
||||
- 27 Outubro - Entrega do 2º exercício de avaliação. Modelação estrutural em Alloy.
|
||||
- 10 Novembro - Entrega do 3º exercício de avaliação. Modelação comportamental em Alloy.
|
||||
- 8 Dezembro - Entrega do 1º exercício de avaliação. Desenvolvimento e verificação de sistemas com estado em Why3.
|
||||
121
content/MFES/T - Aula 2 - 18 Setembro 2023.md
Normal file
121
content/MFES/T - Aula 2 - 18 Setembro 2023.md
Normal file
|
|
@ -0,0 +1,121 @@
|
|||
# Conteúdo
|
||||
1. [[T - Aula 2 - 18 Setembro 2023#1. Intro|Intro]]
|
||||
1. [[T - Aula 2 - 18 Setembro 2023#1.1 SAT|SAT]]
|
||||
2. [[T - Aula 2 - 18 Setembro 2023#1.2 Proposicional Logic (PL)|Lógica Proposicional]]
|
||||
3. [[T - Aula 2 - 18 Setembro 2023#SAT Solvers|SAT Solvers]]
|
||||
|
||||
# 1. Intro
|
||||
*Formal modeling* - formally represent the system and its properties in the syntactic conventions that the tool understands and can process.
|
||||
|
||||
Formal Logic = logical language (logical symbols + non-logical symbols) + semantics +proof system
|
||||
|
||||
### 1.1 SAT
|
||||
<iframe title="Boolean Satisfiability Problem - Intro to Theoretical Computer Science" src="https://www.youtube.com/embed/uAdVzz1hKYY?feature=oembed" height="113" width="200" allowfullscreen="" allow="fullscreen" style="aspect-ratio: 1.76991 / 1; width: 100%; height: 100%;"></iframe>
|
||||
|
||||
The Boolean satisfiability (SAT) problem:
|
||||
|
||||
Find an assignment to the propositional variables of the formula such that the formula evaluates to TRUE, or prove that no such assignment exists.
|
||||
|
||||
|
||||
- SAT is an NP-complete decision problem.
|
||||
- SAT was the first problem to be shown NP-complete.
|
||||
- There are no known polynomial time algorithms for SAT.
|
||||
|
||||
|
||||
Usually SAT solvers deal with formulas in conjunctive normal form (CNF)
|
||||
- **literal**: propositional variable or its negation A, ¬A, B, ¬B, C, ¬C
|
||||
- **clause**: disjuntion of literals. (A _ ¬B _ C)
|
||||
- **conjunctive normal form**: conjuction of clauses. (A _ ¬B _ C) ^ (B _ ¬A) ^ ¬C
|
||||
|
||||
> [!info]+ Cook's theorem(1971)
|
||||
> SAT is NP-complete
|
||||
|
||||
|
||||
## 1.2 Proposicional Logic (PL)
|
||||
|
||||
>[!note] Nota
|
||||
>Esta secção basicamente só contém revisão de conceitos. Aconselha-se a ver a coisa rapidamente, porque é só a formalidade de lógica escrita por extenso.
|
||||
|
||||
Let $A$ be an assignment and let $F$ be a formula. If $A(F) = 1$, then we say **$F$ holds under assignment**, or **$A$ models $F$.**
|
||||
We write A $\models F$ iff $A(F)=1$, and $A \not \models F$ iff $A(F) = 0$.
|
||||
|
||||
|
||||
An assignment is a function $A$ : $V_{prop} \implies {0,1}$ , that assigns to every
|
||||
propositional variable a truth value. An assignment $A$ naturally extends to all formulas, $A$ : **Form** $\implies {0,1}$. The truth value of a formula is computed using **truth tables**:
|
||||
|
||||
| F | $A$ | $B$ | $\neg A$ | $A \land B$ | $A \lor B$ | $A \implies B$ | $A \iff B$ | $\bot$ | $\top$ |
|
||||
| --------- | --- | --- | -------- | ----------- | ---------- | -------------- | ---------- | ------ | ------ |
|
||||
| $A_1 (F)$ | 0 | 1 | 1 | 0 | 1 | 1 | 0 | 0 | 1 |
|
||||
| $A_2 (F)$ | 0 | 0 | 1 | 0 | 0 | 1 | 1 | 0 | 1 |
|
||||
| $A_3 (F)$ | 1 | 1 | 0 | 1 | 1 | 1 | 1 | 0 | 1 |
|
||||
| $A_4 (F)$ | 1 | 0 | 0 | 0 | 1 | 0 | 0 | 0 | 1 |
|
||||
|
||||
|
||||
|
||||
A formula $F$ is:
|
||||
1. **valid** iff it holds under every assignment. We write $\models F$. A valid formula is called a *tautology*.
|
||||
2. **satisfiable** iff it folds (true) under some assignment.
|
||||
3. **unsatisfiable** iff it holds under no assignment. An unsatisfiable formula is called a *contradiction*.
|
||||
4. **refutable** iff it is not valid.
|
||||
|
||||
> [!tip]+ Proposition
|
||||
> $F$ is **valid** iff $\neg F$ is **unsatisfiable**.
|
||||
|
||||
|
||||
- $F \models G$ iff for every assignment $A$, if $A \models F$ then $A \models G$. We say $G$ is a **consequence** of $F$.
|
||||
- $F \equiv G$ iff $F \models G$ and $G \models F$. We say $F$ and $G$ are **equivalent**.
|
||||
- Let $\Gamma = { F_1, F_2, F_3,... }$ be a set of formulas.
|
||||
- $A \models \Gamma$ iff $A \models F_i$ for each formula $F_i$ in $\Gamma$. We say $A$ models $\Gamma$.
|
||||
- $\Gamma \models G$ iff $A \models \Gamma$ implies $A \models G$ for every assignment $A$. We say $G$ is a **consequence** of $\Gamma$.
|
||||
|
||||
> [!tip]+ Proposition
|
||||
> - $F \models G$ iff $\models F \implies G$.
|
||||
> - $\Gamma \models G$ and $\Gamma$ finite iff $\models \land \Gamma \implies G$.
|
||||
>
|
||||
|
||||
- $\Gamma$ is *consistent* or *satisfiable* iff there is an assignment that models $\Gamma$.
|
||||
- We say that $\Gamma$ is inconsistent or unsatisfiable iff there is not consistent and denote this by $\Gamma \models \bot$.
|
||||
|
||||
> [!tip]+ Proposition
|
||||
> - {$F, \neg F$} $\models \bot$
|
||||
> - If $\Gamma \models \bot$ and $\Gamma \subseteq \Gamma '$, then $\Gamma ' \models \bot$
|
||||
> - $\Gamma \models F$ iff $\Gamma, \neg F \models \bot$
|
||||
|
||||
- Formula $G$ is a subformula of formula F if it occurs syntactically within F
|
||||
- Formula G is a strict subformula of F if G is a subformula of $F$ and $G \neg = F$
|
||||
|
||||
|
||||
**Basic Equivalences:**
|
||||
1. $\neg \neg A \equiv A$
|
||||
2. $A \lor A \equiv A$
|
||||
3. $A \land A \equiv A$
|
||||
4. $A \land \neg A \equiv \bot$
|
||||
5. $A \lor \neg A \equiv \top$
|
||||
6. $A \lor B \equiv B \lor A$
|
||||
7. $A \land B \equiv B \land A$
|
||||
8. $A \land \top \equiv A$
|
||||
9. $A \lor \top \equiv \top$
|
||||
10. $A \land \bot \equiv \bot$
|
||||
11. $A \lor \bot \equiv A$
|
||||
12. $A \land (B \lor A) \equiv A$
|
||||
13. $A \land (B \lor C) \equiv (A \land B) \lor (A \land C)$
|
||||
14. $A \lor (B \land C) \equiv (A \lor B) \land (A \lor C)$
|
||||
15. $\neg (A \lor B) \equiv \neg A \land \neg B$
|
||||
16. $\neg (A \land B) \equiv \neg A \lor \neg B$
|
||||
17. $A \implies B \equiv \neg A \lor B$
|
||||
18. $A \iff B \equiv (A \implies B) \land (B \implies A)$
|
||||
|
||||
|
||||
|
||||
|
||||
# 2. SAT Solvers
|
||||
- There are several techniques and algorithms for SAT solving.
|
||||
- Usually SAT solvers receive as input a formula in a specific syntatical format.
|
||||
- SAT solvers deal with formulas in **conjunctive normal form (CNF)**.
|
||||
|
||||
- Most current state-of-the-art SAT solvers are based on the **Davis-Putnam-Logemann-Loveland (DPLL) framework**.
|
||||
|
||||
## 2.1 DPLL Framework
|
||||
The idea is to **incrementally construct an assignment compatible with a CNF**, propagating the implications of the decisions made that are easy to detect and simplifying the clauses.
|
||||
|
||||
A CNF is satisfied by an assignment if all its clauses are satisfied. And a clause is satisfied if at least one of its literals is satisfied.
|
||||
88
content/MFES/TP - Aula 1 - 18 Setembro.md
Normal file
88
content/MFES/TP - Aula 1 - 18 Setembro.md
Normal file
|
|
@ -0,0 +1,88 @@
|
|||
## Ficha 1
|
||||
|
||||
> [!help]+ Ex 1 (Configuração de produtos)
|
||||
> Certos produtos, como é o caso dos automóveis, são altamente personalizáveis, mas podem haver dependências entre as configurações. Os clientes podem não estar cientes de todas essas dependências, e poderão escolher opções de configuração inconsistentes.
|
||||
> Como são muitas configurações e muitas dependências, podemos usar um SAT solver para verificar se o cliente escolhe opções de configuração consistentes. Para isso, podemos seguir os seguintes passos:
|
||||
>
|
||||
> 1. Codificar as dependências entre configurações como uma formula proposicional $\psi$
|
||||
> 2. Codificar as opções selecionadas pelo cliente como uma fórmula proposicional $\phi$.
|
||||
> 3. Usar o SAT solver para verificar se $\psi \land \phi$ não é contraditório.
|
||||
>
|
||||
> Considere agora a seguinte dependência entre as configurações disponíveis para a personalização de um automóvel:
|
||||
>
|
||||
> *"O ar condicionado Thermotronic comfort requer uma bateria de alta capacidade, exceto quando combinado com motores a gasolina de 3,2 litros."*
|
||||
>
|
||||
> Será que um cliente pode escolher o ar condicionado Thermotronic comfort, uma bateria de pequena capacidade e não escolher o motor de 3,2 litros? Como poderia responder a esta pergunta com a ajuda de um SAT solver?
|
||||
>
|
||||
> > [!tip]- Resolução
|
||||
> > Legenda de variáveis utilizadas:
|
||||
> > A - ar condicionado
|
||||
> > B - bateria alta capacidade
|
||||
> > C - motor 3,2 L
|
||||
> >
|
||||
> >$A \land \neg B \implies G \equiv \neg (A \land \neg B) \lor G \equiv \neg A \lor B \lor G$
|
||||
> >
|
||||
> >$(\neg A \lor B \lor G) \land A \land \neg B \land \neg G$ ----- SAT?
|
||||
> >
|
||||
>
|
||||
|
||||
|
||||
> [!help]+ Ex 3 (Configuração de computadores)
|
||||
> Uma loja de eletrónica permite aos seus clientes personalizar o seu computador, escolhendo entre dois modelos de motherboards e dois modelos de monitor. Cada computador tem que ter obrigatoriamente uma única motherboard, um único CPU, uma única placa gráfica e uma única memória RAM. O computador poderá ou não ter um monitor. A personalização do computador deverá obedecer às regras:
|
||||
> 1. A motherboard MB1 quando combinada com a placa gráfica PG1, obriga à utilização da RAM1;
|
||||
> 2. A placa gráfica PG1 precisa do CPU1, exceto quando combinada com a memória RAM2;
|
||||
> 3. O CPU2 só pode estar instalado na motherboard MB2;
|
||||
> 4. O monitor MON1 para poder funcionar precisa da placa gráfca PG1 e da memória RAM2.
|
||||
>
|
||||
>Codifique este problema em lógica proposicional. Assinale claramente o que denota cada variável proposicional que introduzir e escreva um conjunto de fórmulas proposicionais adequado à sua modelação.
|
||||
>
|
||||
> > [!hint]- Resolução
|
||||
> > Legenda de variáveis utilizadas:
|
||||
> > $CPU_1; CPU_2; RAM_1; RAM_2; MB_1; MB_2; PG_1; PG_2; MON_1; MON_2$
|
||||
> >
|
||||
> > Problema modelado:
|
||||
> > 1. $CPU_1 \lor CPU_2$
|
||||
> > 2. $CPU_1 \implies \neg CPU_2$
|
||||
> > 3. $RAM_1 \lor RAM_2$
|
||||
> > 4. $RAM_1 \implies \neg RAM_2$
|
||||
> > 5. $MB_1 \lor MB_2$
|
||||
> > 6. $MB_1 \implies \neg MB_2$
|
||||
> > 7. $PG_1 \lor PG_2$
|
||||
> > 8. $PG_1 \implies \neg PG_2$
|
||||
> >
|
||||
> > 9. $MB_1 \land PG_1 \implies RAM_1$
|
||||
> > 10. $PG_1 \implies CPU_1 \lor RAM_2 \equiv PG_1 \land \neg RAM_2 \implies CPU_1$
|
||||
> > 11. $CPU_2 \implies MB_2$
|
||||
> > 12. $MON_1 \implies PG_1 \land RAM_2$
|
||||
>
|
||||
> Indique, apenas por palavras, como poderia usar um SAT solver para testar as consistências deste conjunto de regras.
|
||||
>
|
||||
> Indique, apenas por palavras, como usaria um SAT solver para se pronuncias quanto à velocidade das seguintes afirmações:
|
||||
> (a) O monitor MON1 só poderá ser usado com uma motherboard MB1.
|
||||
> > [!hint]- Resolução
|
||||
> > ??? $T \models MON_1 \implies MB_1$
|
||||
> > $T, \neg (MON_1 \implies MB_1) UNSAT$
|
||||
> > > [!info] $T \models F$ sse $T, \neg F UNSAT$
|
||||
>
|
||||
> (b) Um cliente pode personalizar o seu computador da seguinte forma: uma motherboard MB2, o CPU1, a placa gráfica PG2 e a memória RAM1.
|
||||
> >[!hint]- Resolução
|
||||
> >$T, MB_2 \land CPU_1 \land PG_2 \land RAM_1$ ---- SAT?
|
||||
|
||||
> [!help]+ Ex 2 (Distribuição de Gabinetes)
|
||||
> Considere que temos 3 gabinetes e queremos distribuir 4 pessoas (Ana=1, Nuno=2, Pedro=3 e Maria=4) por esses gabinetes. Para codificar este problema em lógica proposicional, , vamos ter um conjunto de variáveis proposicionais $x_{p,g}$ com a seguinte semântica:
|
||||
> $x_{p,g}$ é verdade sse a pessoa $p$ ocupa o gabinete $g$, com $p=1..4$ e $g=1..3$
|
||||
>
|
||||
> Considere que forem estipuladas as seguintes regras de ocupação de gabinetes:
|
||||
> 1. Cada pessoa ocupa um único gabinete.
|
||||
> 2. O Nuno e o Pedro não podem partilhar gabinete.
|
||||
> 3. Se a Ana ficar sozinha num gabinete, então o Pedro também terá que ficar sozinho num gabinete.
|
||||
> 4. Cada gabinete só pode acomodar, no máximo, 2 pessoas.
|
||||
>
|
||||
> Escreve um conjunto de fórumlas proposicionais adequado à modelação destas regras.
|
||||
>
|
||||
> >[!tip]- Resolução (por passos)
|
||||
> >**Cada pessoa ocupa só um único gabinete.**
|
||||
> > 1. para cada pessoa p = 1..4
|
||||
> > 2. pelo menos um gabinete: $x_{p1} \lor x_{p2} \lor x_{p3}$
|
||||
> > 3. no máximo 1 gabinete: $x_{p1} \implies \neg x_{p2} \land x_{p3} \equiv x_{p1} \implies \neg (x_{p2} \lor x_{p3} ) \equiv x_{p2} \implies \neg x_{p3}$
|
||||
> > 4.
|
||||
159
content/RAS/T - Aula 2 - 19 Setembro 2023.md
Normal file
159
content/RAS/T - Aula 2 - 19 Setembro 2023.md
Normal file
|
|
@ -0,0 +1,159 @@
|
|||
## Contents
|
||||
1. [[T - Aula 2 - 19 Setembro 2023#Definition of Requirement|Definition of requirement]]
|
||||
2. [[T - Aula 2 - 19 Setembro 2023#Functional requirements|Functional requirements]]
|
||||
3. [[T - Aula 2 - 19 Setembro 2023#Non-functional requirements|Non-functional requirements]]
|
||||
4. [[T - Aula 2 - 19 Setembro 2023#4. User and system requirements|User and system requirements]]
|
||||
5. [[T - Aula 2 - 19 Setembro 2023#Recap|Recap]]
|
||||
|
||||
## 1. Definition of Requirement
|
||||
The requirements express the users necessities and restrictions that are
|
||||
placed on the system.
|
||||
|
||||
A **requirement** is a capacity that a system must possess, to satisfy the
|
||||
users necessities.
|
||||
|
||||
The IEEE 610.12-1990 standard definition divides requirements into
|
||||
two alternatives:
|
||||
1. user needs
|
||||
2. system capacities
|
||||
|
||||
Requirements can be divided into:
|
||||
1. functional requirements
|
||||
2. non-functional requirements
|
||||
|
||||
A r**equirement that for a stakeholder** can be perceived
|
||||
as being **functional**, can be considered as **non-functional**
|
||||
for **a different one**.
|
||||
|
||||
> [!info] A candidate requirement is a requirement that was identified by some elicitation technique.
|
||||
|
||||
|
||||
## 2. Functional requirements
|
||||
|
||||
> [!tip] Definition
|
||||
> A functional requirement describes a functionality to be made
|
||||
available to the users of the system.
|
||||
|
||||
- This type of requirements should not mention any technological issue.
|
||||
- Ideally, functional requirements must be independent of design and
|
||||
implementation aspects.
|
||||
|
||||
> [!note]- Note: Cohesion and Completion
|
||||
> Collectively, the set of functional requirements must be complete and
|
||||
coherent. The set is:
|
||||
> - *coherent*, if there are no contradictions among its elements;
|
||||
> - *complete*, if it considers all the necessities that the client wishes to see
|
||||
satisfied.
|
||||
>
|
||||
> Defining complete requirements is the most difficult attribute to
|
||||
achieve or evaluate.
|
||||
|
||||
> [!note]- Note: Implicit and Explicit Requirements
|
||||
> Implicit requirements are referred like that because the client may not be aware about these requirements.
|
||||
>
|
||||
> An **implicit requirement** is a requirement included by the development team, based on the domain knowledge that it possesses, in spite of not having been explicitly requested by the stakeholders.
|
||||
>
|
||||
> An **explicit requirement** refers to a requirement that was requested by the clients and that is represented in the documentation.
|
||||
|
||||
|
||||
## 3. Non-functional requirements
|
||||
|
||||
> [!tip] Definition
|
||||
> A non-functional requirement corresponds to a set of restrictions
|
||||
imposed on the system to be developed.
|
||||
|
||||
- Alternative terms: quality requirement or quality attribute
|
||||
- It establishes how attractive, fast, or reliable the system is.
|
||||
- It includes time constraints, restrictions in the development process, or
|
||||
adoption of standards.
|
||||
|
||||
> [!example]- Example: Technological restriction
|
||||
> The product must be developed in C++.
|
||||
|
||||
> [!info] **A non-functional requirement does not change the essence of the system functionalities.**
|
||||
|
||||
|
||||
- Non-functional requirements are applicable to the system as a whole
|
||||
and not just to some of its parts, as, generally, non-functional requirements **cannot be modularized**.
|
||||
|
||||
- The non-functional requirements are frequently **emergent properties** of the system at hand. *An emergent property of a system is a property that can be associated with the system as a whole, but not individually to each of its components.*
|
||||
- *Reliability* is a good example of an emergent property.
|
||||
|
||||
|
||||
> [!info] **Non-functional requirements are crucial to decide the system architecture.**
|
||||
|
||||
|
||||
|
||||
### 3.1 Classification of non-functional requirements
|
||||
|
||||
> [!tip]- Classification: Sommerville (2010)
|
||||
> - **product requirements**: characterise aspects of the behaviour of the system itself (*reliability, performance, efficiency, portability, usability, testability, and readability*).
|
||||
> - **organisational requirements**: come from strategies and procedures established in the context of the manufacturing process of the system or the client organisation (process standards and implementation requirements).
|
||||
> - **external requirements**: have origin in external factors to the system and the development process (interoperability, legal, and ethical requirements).
|
||||
|
||||
> [!tip]- Classification: Roberson and Roberson (2006)
|
||||
> - **appearance**: the aspect and the aesthetics of the system;
|
||||
> - **usability**: the easiness of utilization of the system and everything that permits a more friendly user experience;
|
||||
> - **performance**: aspects of speed, real-time, storage capacity, and execution correction;
|
||||
> - **operational**: characteristics about what the system must do to work correctly in the environment where it is inserted;
|
||||
> - **maintenance and support**: attributes that allow the system to be repaired or improved and new functionalities to be added;
|
||||
> - **security**: issues related to access, confidentiality, protection, and integrity of the data;
|
||||
> - **cultural and political**: factors related to the stakeholders culture and habits;
|
||||
> - **legal**: laws that apply to the system so that it can operate.
|
||||
|
||||
#### 3.1.1 Usability
|
||||
- **Ease of use** is related to the efficiency of utilizing a system and with the mechanisms that reduce the errors made by the users.
|
||||
- **Personalization** is associated with the capacity of adapting the system to the tastes of the users.
|
||||
- **Ease of learning** is concerned with the way users are trained to use the system.
|
||||
- **Accessibility** indicates how easy it is to use the system, for people who
|
||||
are somehow physically or mentally disabled.
|
||||
|
||||
> [!example]- Example: Usability requirements
|
||||
> 1. The product shall be easy to use for illiterate persons.
|
||||
> 2. The product shall be intuitive to use for children with 4 years old.
|
||||
> 3. The product shall be usable by visually impaired persons.
|
||||
|
||||
#### 3.1.2 Maintenance and support
|
||||
- System maintenance is divided into four types: preventive, corrective, perfective, and adaptive.
|
||||
- **Modifiability** is related to maintenance and is dependent on how easy it is to locate the components that must be changed.
|
||||
|
||||
> [!example]- Example: Maintenance and support requirements
|
||||
> 1. The source code of the product programs should contain comments.
|
||||
> 2. The product must be prepared to be translated to any language.
|
||||
|
||||
#### 3.1.3 Legal
|
||||
> [!example]- Example: Legal requirements
|
||||
> 1. The product shall be aligned with the PMBoK guide.
|
||||
> 2. The product shall be certified by the Taxing Authority.
|
||||
> 3. The product shall fulfil with the copyright.
|
||||
|
||||
|
||||
|
||||
## 4. User and system requirements
|
||||
|
||||
A **user requirement** represents:
|
||||
1. a functionality that the system is expected to provide to its users;
|
||||
2. a restriction that is applicable to the operation of that system.
|
||||
|
||||
- These requirements are related to the problem domain.
|
||||
- They are normally expressed without great mathematical rigour, using natural language and informal diagrams.
|
||||
|
||||
|
||||
A **system requirement** constitutes a more detailed specification of a requirement, being generally a formal model of the system. These requirements are oriented towards the solution domain, and are documented in a more technical language than the one
|
||||
adopted for the user requirements.
|
||||
|
||||
### 4.1 Problem domain
|
||||
- The requirements result from necessities that exist in the problem domain to be addressed.
|
||||
- User requirements should be described with the problem domain terminology.
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
# Recap
|
||||
1. Requirements represent the necessities of the users and the constraints that are applied to a system and that must be considered throughout the development.
|
||||
2. The requirements can be classified, according to a first criterion, as either functional or non-functional.
|
||||
3. Non-functional requirements are divided in 8 different types: appearance, usability, performance, operational, maintenance and support, security, cultural and political, and legal.
|
||||
4. The requirements can be designated as either user or system requirements.
|
||||
5. User requirements are related to the problem domain and are usually expressed in a natural language.
|
||||
6. A system requirement is oriented towards the solution domain and is a detailed specification of a requirement, generally in the form of a formal model of the system.
|
||||
10
content/index.md
Normal file
10
content/index.md
Normal file
|
|
@ -0,0 +1,10 @@
|
|||
Basicamente, isto é uma sopa de letras com alguma lógica por detrás (mas não muita). Abandonem as expectativas. :)
|
||||
|
||||
## Conteúdo
|
||||
### Ano 1 (Mestrado)
|
||||
1. [[MFES - UC Details| (MFES) Métodos Formais de Engenharia de Software]]
|
||||
2. (ASCN) Aplicações e Serviços de COmpitação em Nuvem
|
||||
3. (RAS) Requisitos e Arquiteturas de Software
|
||||
4. (CP) Computação Paralela
|
||||
5. (DAA) Dados e Aprendizagem Automática
|
||||
6. (ESR) Engenharia de Serviços em Rede
|
||||
|
|
@ -78,6 +78,7 @@
|
|||
"remark-smartypants": "^2.0.0",
|
||||
"rimraf": "^5.0.1",
|
||||
"serve-handler": "^6.1.5",
|
||||
"shiki": "^0.14.4",
|
||||
"source-map-support": "^0.5.21",
|
||||
"to-vfile": "^7.2.4",
|
||||
"toml": "^3.0.0",
|
||||
|
|
|
|||
|
|
@ -9,7 +9,7 @@ const config: QuartzConfig = {
|
|||
analytics: {
|
||||
provider: "plausible",
|
||||
},
|
||||
baseUrl: "quartz.jzhao.xyz",
|
||||
baseUrl: "notes.flup.dev",
|
||||
ignorePatterns: ["private", "templates", ".obsidian"],
|
||||
defaultDateType: "created",
|
||||
theme: {
|
||||
|
|
|
|||
Loading…
Reference in a new issue