From 57be99fe7e12148907488988410724a00ea22438 Mon Sep 17 00:00:00 2001 From: ivan-gavran Date: Mon, 27 May 2024 20:27:42 +0200 Subject: [PATCH 1/3] 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 e034697778281492142210d785135b7b241ec1b6 Mon Sep 17 00:00:00 2001 From: Ivan Gavran Date: Tue, 28 May 2024 00:07:14 +0200 Subject: [PATCH 2/3] 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 c817c2bcde1a62a875f6957049885800240057da Mon Sep 17 00:00:00 2001 From: ivan-gavran Date: Tue, 28 May 2024 00:16:52 +0200 Subject: [PATCH 3/3] switching MB Testing > MB Techniques, for a broader picture --- 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 87918536..33838ed1 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) 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. +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: