Courses
- Introduction to Software Engineering (10014) תקציר הקורס:
- Software Systems Modeling (10148) תקציר הקורס:
- Seminar (10400) תקציר הקורס:
Abstract:
The first digital computer was built for the US Army in 1946.
High-level programming languages appeared in the 1950s.
Within a quarter century, we already faced what is known as the “software crisis”.
The crisis did not occur because software was not f?unctioning properly but rather because of problems related to the software development process, and the growing demand for complex software systems. The software crisis manifests itself in many problems: lack of well defined requirements; frequently changing requirements; poorly estimated costs and budgets; programmer productivity that cannot keep up with demand; and software of insufficient quality.
Software Engineering was developed in order to solve the problems that characterize the software crisis, and it encompasses the entire software development life cycle.Abstract:
The module consists of two parts. In the first part we will study simple reactive systems and learn how to model them as transition systems and how to express properties using temporal logic formulas. We will then learn how to use a model checker to check if the models satisfy the properties. In the second part we will learn how to describe information systems using relational logic and how to express business rules and structural invariants using relational logic formulas. Finally, we will learn how to use the Alloy analyzer to check that the model satisfies the business rules and structural invariants.Abstract:
The term formal methods refers to languages and methods that allow precise modeling of systems at various levels of abstraction, requirements to be formulated for them and the fulfillment of these requirements to be reliably analyzed.
Formal methods are used in software engineering to enable precise and unambiguous specifications, rigorous design, and formal verification of systems, reducing the likelihood of errors that could lead to failures in critical applications.
This seminar introduces students to formal methods, emphasizing the importance of these methods in ensuring software correctness, reliability, and security.
At the seminar, we will cover various topics in formal methods throughout the software development lifecycle.