From fe7d4a7ad724b8f0c95de07a36c205c02751ddd0 Mon Sep 17 00:00:00 2001 From: ivan-gavran Date: Mon, 27 May 2024 20:27:42 +0200 Subject: [PATCH 1/5] added two high-level paragraphs on model-based techniques --- jekyll/index.md | 18 +++++++++++++++++- 1 file changed, 17 insertions(+), 1 deletion(-) diff --git a/jekyll/index.md b/jekyll/index.md index 01e00e26..87918536 100644 --- a/jekyll/index.md +++ b/jekyll/index.md @@ -6,9 +6,25 @@ description: Model Based Testing in Informal Systems has_children: true --- +# Model Based Testing +Building a model of our software gives us a couple of elegant and efficient ways to increase confidence in its correctness. +Modeling languages (such as [TLA+](https://lamport.azurewebsites.net/tla/tla.html) or [Quint](https://github.com/informalsystems/quint)) are supported by _model checkers_, which enable us to reason about the model's properties. +We can specify desired properties and verify that the model satisfies them, or we can generate a large number of tests directly from the model and run them against the implementation. + +A model can be written even before the development starts. +This enables finding problems early on, in the development phase. + +Besides being a tool for finding difficult-to-spot problems, models serve as high-level, yet precise and executable specifications. + + # Model Based Testing @ Informal Systems -At Informal Systems we aim to incorporate formal methods into everyday development practice. On the practical side, we develop tools and techniques that help developers to increase confidence in their code via automated generation and execution of tests derived from TLA+ models. +At Informal Systems, we use model-based techniques both in our development practice and as a part of our security audit services. +We develop and maintain the following tools that make model-based techniques easy to incorporate in the development and auditing practice: + - [Quint](https://github.com/informalsystems/quint), a modern modeling language + - [Apalache](https://apalache.informal.systems/), a symbolic model checker + - [Modelator](https://github.com/informalsystems/modelator), a tool that enables automatic generation of tests from models + - [cosmwasm-to-quint](https://github.com/informalsystems/cosmwasm-to-quint), a tool for generating Quint model stubs and accompanying tests directly from [CosmWasm](https://cosmwasm.com/) contracts From 0b18a40d6b1efd11be02975bff3fe6b7063b7eee Mon Sep 17 00:00:00 2001 From: Ivan Gavran Date: Tue, 28 May 2024 00:07:14 +0200 Subject: [PATCH 2/5] Update jekyll/index.md: review suggestion TLA+ and Quint Co-authored-by: Gabriela Moreira --- jekyll/index.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/jekyll/index.md b/jekyll/index.md index 87918536..c5e145cc 100644 --- a/jekyll/index.md +++ b/jekyll/index.md @@ -8,7 +8,7 @@ has_children: true # Model Based Testing Building a model of our software gives us a couple of elegant and efficient ways to increase confidence in its correctness. -Modeling languages (such as [TLA+](https://lamport.azurewebsites.net/tla/tla.html) or [Quint](https://github.com/informalsystems/quint)) are supported by _model checkers_, which enable us to reason about the model's properties. +Modeling languages (such as [TLA+](https://lamport.azurewebsites.net/tla/tla.html) and [Quint](https://github.com/informalsystems/quint)) are supported by _model checkers_, which enable us to reason about the model's properties. We can specify desired properties and verify that the model satisfies them, or we can generate a large number of tests directly from the model and run them against the implementation. A model can be written even before the development starts. From 53065d92b1bb4cd7a8f472c85486bdb9c1e04767 Mon Sep 17 00:00:00 2001 From: ivan-gavran Date: Tue, 28 May 2024 00:16:52 +0200 Subject: [PATCH 3/5] merge --- jekyll/README.md | 2 +- jekyll/_config.yml | 2 +- jekyll/docs/model.md | 2 +- jekyll/docs/modelator.md | 2 +- jekyll/index.md | 10 +++++----- 5 files changed, 9 insertions(+), 9 deletions(-) diff --git a/jekyll/README.md b/jekyll/README.md index d46d9212..d3def5ae 100644 --- a/jekyll/README.md +++ b/jekyll/README.md @@ -1,4 +1,4 @@ -# Jekyll Website for Model Based Testing +# Jekyll Website for Model Based Techniques The website is live at [https://mbt.informal.systems](https://mbt.informal.systems) diff --git a/jekyll/_config.yml b/jekyll/_config.yml index eff04ede..b421e58a 100644 --- a/jekyll/_config.yml +++ b/jekyll/_config.yml @@ -1,4 +1,4 @@ -title: Model Based Testing +title: Model Based Techniques description: Part of Informal Systems baseurl: "" url: "https://mbt.informal.systems" diff --git a/jekyll/docs/model.md b/jekyll/docs/model.md index f86de8c4..96732194 100644 --- a/jekyll/docs/model.md +++ b/jekyll/docs/model.md @@ -2,7 +2,7 @@ title: Model extraction description: Extract abstract model from your implementation layout: default -parent: Model Based Testing +parent: Model Based Techniques nav_order: 2 --- --> diff --git a/jekyll/docs/modelator.md b/jekyll/docs/modelator.md index db1e5607..2c72f828 100644 --- a/jekyll/docs/modelator.md +++ b/jekyll/docs/modelator.md @@ -2,7 +2,7 @@ title: Modelator description: Tool to model based testing from Informal Systems layout: default -parent: Model Based Testing +parent: Model Based Techniques nav_order: 3 --- diff --git a/jekyll/index.md b/jekyll/index.md index c5e145cc..c7d16a6f 100644 --- a/jekyll/index.md +++ b/jekyll/index.md @@ -1,15 +1,15 @@ --- layout: default -title: Model Based Testing +title: Model Based Techniques nav_order: 1 -description: Model Based Testing in Informal Systems +description: Model Based Techniques at Informal Systems has_children: true --- -# Model Based Testing +# Model Based Techniques for Software Correctness Building a model of our software gives us a couple of elegant and efficient ways to increase confidence in its correctness. Modeling languages (such as [TLA+](https://lamport.azurewebsites.net/tla/tla.html) and [Quint](https://github.com/informalsystems/quint)) are supported by _model checkers_, which enable us to reason about the model's properties. -We can specify desired properties and verify that the model satisfies them, or we can generate a large number of tests directly from the model and run them against the implementation. +We can specify desired properties and verify that the model satisfies them. We can also generate a large number of tests directly from the model and run them against the implementation. A model can be written even before the development starts. This enables finding problems early on, in the development phase. @@ -17,7 +17,7 @@ This enables finding problems early on, in the development phase. Besides being a tool for finding difficult-to-spot problems, models serve as high-level, yet precise and executable specifications. -# Model Based Testing @ Informal Systems +# Model Based Techniques @ Informal Systems At Informal Systems, we use model-based techniques both in our development practice and as a part of our security audit services. We develop and maintain the following tools that make model-based techniques easy to incorporate in the development and auditing practice: From 7c7e9e3f2116717b4e260a18a4da75d5d2f53860 Mon Sep 17 00:00:00 2001 From: ivan-gavran Date: Tue, 28 May 2024 00:16:52 +0200 Subject: [PATCH 4/5] fixed conflict From cdfa47e897f46ae6daa26e36ec8f870179112e14 Mon Sep 17 00:00:00 2001 From: Rano | Ranadeep Date: Mon, 27 May 2024 19:40:28 -0400 Subject: [PATCH 5/5] grammar and formatting --- jekyll/index.md | 8 ++------ 1 file changed, 2 insertions(+), 6 deletions(-) diff --git a/jekyll/index.md b/jekyll/index.md index c7d16a6f..397800f8 100644 --- a/jekyll/index.md +++ b/jekyll/index.md @@ -14,18 +14,14 @@ We can specify desired properties and verify that the model satisfies them. We c A model can be written even before the development starts. This enables finding problems early on, in the development phase. -Besides being a tool for finding difficult-to-spot problems, models serve as high-level, yet precise and executable specifications. +Besides being a tool for finding difficult-to-spot problems, models serve as high-level yet precise and executable specifications. # Model Based Techniques @ Informal Systems At Informal Systems, we use model-based techniques both in our development practice and as a part of our security audit services. -We develop and maintain the following tools that make model-based techniques easy to incorporate in the development and auditing practice: +We develop and maintain the following tools that make model-based techniques easy to incorporate into the development and auditing practice: - [Quint](https://github.com/informalsystems/quint), a modern modeling language - [Apalache](https://apalache.informal.systems/), a symbolic model checker - [Modelator](https://github.com/informalsystems/modelator), a tool that enables automatic generation of tests from models - [cosmwasm-to-quint](https://github.com/informalsystems/cosmwasm-to-quint), a tool for generating Quint model stubs and accompanying tests directly from [CosmWasm](https://cosmwasm.com/) contracts - - - -