searchindex.en.js

var relearn_searchindex = [
  {
    "breadcrumb": "The ABS Language \u003e Documentation \u003e Examples",
    "content": "One reason to model systems is to gain insight into and predict complex behavior. Ideally, the components of the system are reasonably easy to understand in isolation, while assembling them together results in surprising behavior that can provide insight or support for a theory about the whole system.\nThe Monty Hall Problem The Monty Hall problem (Monty Hall problem - Wikipedia) states:\nSuppose you’re on a game show, and you’re given the choice of three doors: Behind one door is a car; behind the others, goats. You pick a door, say No. 1, and the host, who knows what’s behind the doors, opens another door, say No. 3, which has a goat. He then says to you, “Do you want to pick door No. 2?” Is it to your advantage to switch your choice?\nThe “intuitive” assumption from many people would be that changing one’s guess cannot make a difference to the outcome. But is this true? Let us model this system and find out!\nThe code for this example can be found at https://github.com/abstools/absexamples/tree/master/collaboratory/examples/monty-hall/\nModeling the Participants Each round in the game is played between a participant and a host. First the guest submits an initial guess to the host. The host answers by ruling out one of the two other doors as being the correct one. Then, the participant decides on which door to open according to their strategy: either decide to open the original door, or switching to the other closed door. The following sequence diagram illustrates the interaction:\nsequenceDiagram participant Host participant Contestant Contestant-\u003e\u003eHost: guess(door1) Host-\u003e\u003eContestant: goat_door Contestant-\u003e\u003eHost: open(door2) Note right of Contestant: door2 == door1\u003cbr/\u003eor door2 != door1\u003cbr/\u003edepending on strat Host-\u003e\u003eContestant: prize Note right of Contestant: prize is Car or Goat The Host For simplicity, we model the three doors as the numbers 0..2. The host has two methods: guess, which takes a door and returns another door that is definitely the wrong answer (the host is trustworthy). The method open takes a door and returns its content: Car or Goat.\ndata Prize = Car | Goat; interface Host { Int guess(Int door_guess); Prize open(Int door); } class Host implements Host { Int winning_door = random(3); // 0..2 List\u003cInt\u003e losing_doors = without(list[0, 1, 2], winning_door); Int guess(Int door_guess) { return (when door_guess == winning_door then nth(losing_doors, random(2)) else head(without(losing_doors, door_guess))); } Prize open(Int door) { return when door == winning_door then Car else Goat; } } The Contestants The Contestants “drive” the interaction. The method play implements the sequence of interactions shown above: the contestant picks a number, submits it to the host, receives information about another door, and finally asks the host to open the chosen door. Each contestant keeps track of the number of rounds and wins they have played.\nThe code below shows the contestant that switches their guess after shown the incorrect door; the non-switching contestant is similar except for one line.\ninterface Contestant { Unit play(Host host); Unit printSummary(); } class SwitchingContestant implements Contestant { Int nPlays = 0; Int nWins = 0; Unit play(Host host) { Int pick_door = random(3); Int goat_door = await host!guess(pick_door); Int final_door = head(without(without(list[0, 1, 2], pick_door), goat_door)); Prize prize = await host!open(final_door); nPlays = nPlays + 1; if (prize == Car) nWins = nWins + 1; } Unit printSummary() { println(`I always switched, won $nWins$ out of $nPlays$ rounds.`); } } Running the Example Since we want to investigate whether the results for switching and non-switching strategies are different, we create one participant of each type and let them play against 1000 hosts:\n{ Int nRounds = 1000; Contestant swc = new SwitchingContestant(); Contestant nsc = new NonSwitchingContestant(); while (nRounds \u003e 0) { nRounds = nRounds - 1; Host host = new Host(); await swc!play(host); await nsc!play(host); } swc.printSummary(); nsc.printSummary(); } Running the model produces output similar to the following:\nI always switched, won 628 out of 1000 rounds. I never switched, won 333 out of 1000 rounds. As we see, the intuitive expectation about the outcome is not supported by the simulation! The composition of simple components with understandable behavior can indeed lead to observation of surprising behavior, which is the goal of modeling a system.",
    "description": "Modeling simple behavior, getting complex results.",
    "tags": [],
    "title": "The Monty Hall Problem",
    "uri": "/documentation/examples/monty-hall/index.html"
  },
  {
    "breadcrumb": "The ABS Language \u003e Getting Started",
    "content": "Many of the tools can be run from the command line. This page describes how to run various tools on a local machine.\nInstalling Dependencies The ABS compiler is contained in a single file called absfrontend.jar.\nRunning the ABS compiler requires Java (version 21 or greater) and Erlang (version 26 or greater) installed. Java can be downloaded, e.g., from https://adoptopenjdk.net. Erlang is available at https://www.erlang.org/downloads (but also check below for platform-specific instructions).\nInstalling dependencies on MacOS On MacOS, the homebrew package manager can be used to install the dependencies. After installing homebrew, run the following commands in a terminal:\nbrew install erlang git openjdk export PATH=\"/opt/homebrew/opt/openjdk/bin:$PATH\" Installing dependencies on Windows On windows, the chocolatey package manager can be used to install the dependencies. First install chocolatey following the instructions at https://chocolatey.org/install, then run the following command in a terminal with Administrator rights:\nchoco install openjdk21 git erlang visualstudio2019buildtools To compile the ABS toolchain, make sure to run the command ./gradlew build from a developer shell (Start -\u003e Visual Studio 2019 -\u003e Developer PowerShell for VS 2019).\nInstalling dependencies on Linux On Linux, check if your distribution offers the necessary programs pre-packaged in the version needed (JDK21, Erlang \u003e= 26, a C compiler); otherwise download from the distribution pages linked above.\nUsing a pre-built ABS compiler A pre-built absfrontend.jar of the current release of ABS is always linked from https://github.com/abstools/abstools/releases/latest. It can be invoked with java -jar absfrontend.jar --help. (Java and Erlang still need to be installed to run ABS, as above.)\nTo compile an ABS model model.abs, invoke the compiler with java -jar absfrontend.jar --erlang model.abs, then run the model with ./gen/erl/run.\nUsing Docker to run the ABS compiler The latest released ABS compiler is always published as a docker image called abslang/absc:latest. To use this image, first install the docker tool from https://www.docker.com/products/docker-desktop or via your operating system’s package manager.\nTo install or update the docker image of the ABS compiler, run docker pull abslang/absc:latest. Then, run docker run --rm abslang/absc:latest --help – you should see the help output of the ABS compiler.\nTo compile an ABS model model.abs in the current directory, invoke the compiler with the following command:\ndocker run --rm -v \"$PWD\":/usr/src -w /usr/src abslang/absc:latest --erlang model.abs To run the model after compiling, either run ./gen/erl/run (if the host machine has erlang installed), or run the model inside docker with the following command:\ndocker run --rm -v \"$PWD\":/usr/src -w /usr/src --entrypoint /usr/src/gen/erl/run abslang/absc Note that using the Model API of a model running inside a docker container requires additional parameters to make the listening port visible on the host system. To run the Model API on port 8080, use the following command:\ndocker run --rm -v \"$PWD\":/usr/src -p 8080:8080 -w /usr/src --entrypoint /usr/src/gen/erl/run abslang/absc -p 8080 Compiling the ABS compiler from source To compile the ABS compiler from source, clone the git repository and run gradle (after installing the necessary dependencies):\n# on Linux, macOS git clone https://github.com/abstools/abstools.git cd abstools ./gradlew assemble frontend/bin/absc --help # on Windows git clone \"https://github.com/abstools/abstools.git\" cd abstools .\\gradlew assemble frontend\\bin\\absc.bat --help At the end of these commands, you should see the help output of the ABS compiler.\nThe directory abstools/frontend/bin contains convenience scripts absc (for Linux, macOS, other Unix systems) and absc.bat (for Windows) that invoke the ABS compiler. This directory can be added to the PATH environment variable if desired.\nTo compile an ABS model model.abs, invoke the compiler with absc --erlang model.abs, then run the model with ./gen/erl/run.\nInstalling Crowbar For a local installation of the Crowbar verification systems, either download a prepackaged jar file, or compile the code locally. Crowbar requires Java \u003e= 1.8 and an SMT-Solver to run. On an Ubuntu machine, run the following to install Crowbar and run it on an example file:\nsudo apt-get install z3 mkdir crowbar cd crowbar git clone https://github.com/Edkamb/crowbar-tool.git . ./gradlew assemble java -jar build/libs/crowbar.jar --full examples/account.abs The expected output should end in the lines\n... Crowbar : Final verification result: true Crowbar : Verification time: ... Crowbar : Total number of branches: 6 Installing KeY-ABS For a local installation of the KeY-ABS theorem prover, install Java 8. Then, download KeY-ABS from http://i12www.ira.uka.de/key/key-abs/key-abs.zip. Unzipping that downloaded file and double-clicking on the key.jar file should start KeY-ABS. To start from the command line, use:\njava -jar key.jar",
    "description": "Many of the tools can be run from the command line.  This page describes how to run various tools on a local machine.",
    "tags": [],
    "title": "Installing Command-Line Tools",
    "uri": "/getting_started/local-install/index.html"
  },
  {
    "breadcrumb": "The ABS Language",
    "content": "DESIGN PRINCIPLES OF ABS ABS targets the modeling of software systems that are concurrent, distributed, object-oriented, built from components, and highly reusable. To achieve the latter, we follow the arguably most successful software reuse methodology in practice: software product families or software product lines [35], see also the Product Line Hall of Fame. ABS supports the modeling of variability in terms of feature models as a first-class language concept. ABS thus provides language-based support for product line engineering (PLE).\nAs an abstract language ABS is well suited to model software that is supposed to be deployed in a virtualized environment. To close the gap between design and deployment it is necessary to represent low-level concepts such as system time, memory, latency, or scheduling at the level of abstract models. In ABS this is possible via a flexible and pluggable notation called deployment components, covered in detail in [24].\nABS is not merely a modeling notation, but it arrives with an integrated tool set that helps to automate the software engineering process. Tools are useless, however, unless they ensure predictability of results, interoperability, and usability. A fundamental requirement for the first two criteria is a uniform, formal semantics. But interoperability also involves the capability to connect with other notations than ABS. This is ensured by providing numerous language interfaces from and to ABS. These are realized by various import, export, and code generation tools.\nArguably the most important criterion for tools, however, is usability. This tutorial is not the place to embark on a full discussion of what that entails, but it should be indisputable that automation, scalability, and integration are of the utmost importance. To ensure the first two of these qualities, the HATS project adopted as a central principle to develop ABS in tandem with its tool set. This is not merely a historical footnote, but central to an understanding of the trade-offs made in the design of the ABS language. For most specification and programming languages their (automatic) analyzability is considered in hindsight and turns out not to be scalable or even feasible. With ABS, the slogan of design for verifiability that originated in the context of hardware description languages [30], has been systematically applied to a software modeling language. For example, the concurrency model of ABS is designed such that it permits a compositional proof system [3], the reuse principle employed in ABS is chosen in such a way that incremental verification is possible [21], etc. Many formal methods tools focus on analysis, in particular, on verification. Functional verification, model checking, test case generation, and resource estimation are supported by ABS tools as well. Just as important as analytic methods, specifically in a model-based context, are generative ones: ABS is fully executable (albeit in a non-deterministic manner) and supports code generation to Erlang and Maude.\nABS language architecture\nIn addition to the simulation tools, a number of analysis and generation tools are available as well. An overview of the ABS tool suite is given in [42].",
    "description": "DESIGN PRINCIPLES OF ABS ABS targets the modeling of software systems that are concurrent, distributed, object-oriented, built from components, and highly reusable. To achieve the latter, we follow the arguably most successful software reuse methodology in practice: software product families or software product lines [35], see also the Product Line Hall of Fame. ABS supports the modeling of variability in terms of feature models as a first-class language concept. ABS thus provides language-based support for product line engineering (PLE).",
    "tags": [],
    "title": "Overview",
    "uri": "/overview/index.html"
  },
  {
    "breadcrumb": "The ABS Language \u003e Documentation \u003e Tutorials",
    "content": "This tutorial is partially adapted but needs updating to the newest language and tool features\n1 Installation of the ABS Eclipse Plugin ABS fills a gap in the landscape of software modeling languages. It is situated between architectural, design-oriented, foundational, and implementation-oriented languages [25] For trying out the examples provided in this tutorial you will need the ABS Eclipse plugin. To install it, follow the simple instructions at http://tools.hats-project.eu/eclipseplugin/installation.html. You will need at least Eclipse version 3.6.2 and it is recommended to work with a clean installation. The example project used throughout this tutorial is available as an archive from http://www.hats-project.eu/sites/default/files/TutorialExample.zip. To install, unzip the archive file into a directory /mypath/Account. Then create a new ABS Project and import the directory file contents into Eclipse workspace in the usual way. After opening a few files in the editor you should see a screen similar to the one here:\n2 Design Principles of ABS ABS targets software systems that are concurrent, distributed, object-oriented, built from components, and highly reusable. To achieve the latter, we follow the arguably most successful software reuse methodology in practice: software product families or software product lines [35], see also the Product Line Hall of Fame. To this end, ABS supports the modeling of variability in terms of feature models as a first-class language concept. As shown in Sect. 8, ABS thus provides language-based support for product line engineering (PLE). As an abstract language ABS is well suited to model software that is supposed to be deployed in a virtualized environment. To close the gap between design and deployment it is necessary to represent low-level concepts such as system time, memory, latency, or scheduling at the level of abstract models. In ABS this is possible via a flexible and pluggable notation called deployment components. This goes beyond the present, introductory tutorial, but is covered in detail in the chapter by Johnsen in this volume [24]. ABS is not merely a modeling notation, but it arrives with an integrated tool set that helps to automate the software engineering process. Tools are useless, however, unless they ensure predictability of results, interoperability, and usability. A fundamental requirement for the first two criteria is a uniform, formal semantics. But interoperability also involves the capability to connect with other notations than ABS. This is ensured by providing numerous language interfaces from and to ABS as shown in below. These are realized by various import, export, and code generation tools, several of which are discussed below.\nArguably the most important criterion for tools, however, is usability. This tutorial is not the place to embark on a full discussion of what that entails, but it should be indisputable that automation, scalability, and integration are of the utmost importance. To ensure the first two of these qualities, the HATS project adopted as a central principle to develop ABS in tandem with its tool set. This is not merely a historical footnote, but central to an understanding of the trade-offs made in the design of the ABS language. For most specification and programming languages their (automatic) analyzability is considered in hindsight and turns out not to be scalable or even feasible. With ABS, the slogan of design for verifiability that originated in the context of hardware description languages [30], has been systematically applied to a software modeling language. For example, the concurrency model of ABS is designed such that it permits a compositional proof system [3], the reuse principle employed in ABS is chosen in such a way that incremental verification is possible [21], etc. Many formal methods tools focus on analysis, in particular, on verification. Functional verification, model checking, test case generation, and resource estimation are supported by ABS tools as well. Just as important as analytic methods, specifically in a model-based context, are generative ones: ABS is fully executable (albeit in a non-deterministic manner) and supports code generation to Java, Scala, and Maude. In addition, it is possible to learn ABS models from observed behavior [16]. Regarding integration, the tool set around the ABS language is realized as a set of plugins for the popular Eclipse IDE. These plugins realize the ABS\nModeling Perspective (see Fig. 2) and the ABS Debug Perspective (see Fig. 8), which provide the same functionality as their Java counterparts, that is, parsing, syntax highlighting, parse error location, symbol lookup, compilation, building, runtime configurations, interactive debugging, etc. In addition to these standard development tools, however, a number of analysis and generation tools are available as well. Some of these, for example, Java code generation or type inference are illustrated below. An overview of the ABS tool suite is given in [42].\n3 Architecture of ABS The architecture of ABS has been organized as a stack of clearly separated layers as illustrated in Fig. 4. In the design we strove for\nan attractive, easy-to-learn language with a syntax that is familiar to many developers and to provide maximal separation of concern (orthogonality) among different concepts. The four bottom layers provide a modern programming language based on a combination of algebraic data types (ADTs), pure functions, and a simple imperative-OO language. The idea is that anyone familiar with either Java and Haskell or with Scala is able to grasp this part of ABS immediately, even though ABS is considerably simpler than any of these languages. The next two layers realize tightly coupled and distributed concurrency, respectively. The concurrency and synchronization constructs are designed in a way to permit a compositional proof theory for functional verification in a program logic [3]. Standard contracts are used for functional specification of sequential programs and behavioral interfaces over sets of histories are used for specifying concurrent programs, see also the paper by Poetzsch-Heffter in this volume [34]. The language layers up to here are often called Core ABS. Above these are orthogonal extensions for product line engineering, deployment components, and runtime components that allow to model mobile code. The latter are not discussed in this volume, but are described in [28]. As mentioned above, ABS is a fully executable language. Nevertheless, abstraction is achieved in a number of ways: first of all, ABS contains only five built-in datatypes—everything else is user-defined. The rationale is that no premature decision on the properties of datatypes is enforced, which helps to create implementation-independent models. Second, functions on datatypes can be underspecified. The modeler has the alternative to return abstract values or to leave case distinctions incomplete. The latter may result in runtime errors, but is nevertheless useful for simulation, test generation or verification scenarios. Third, the scheduling of concurrent tasks as well as the order of queuing messages is non-deterministic. Of course, one might want to give full implementation details at some time. This is possible by refining an ADT into an implemented class or by realizing it in Java via the foreign language interface available in ABS (Sect. 7. Concrete schedulers can be specified via deployment components [24, 32]. Crucially, the abstraction capabilities of ABS allow to specify partial behavior during early design stages, such as feature analysis, without committing to implementation details. This lends support, for example, to rapid prototyping or to the early analysis of consequences of design decisions. ABS has been designed as a compact language. Each layer has no more first-class concepts than are needed to ensure usability (including some syntactic sugar). This does not mean, however, that ABS is a small language: the ABS grammar has considerably more non-terminals than that of Java! The reason is that ABS features several language concepts that are simply not present in Java. In the final analysis, this reflects the ambition of ABS to cover the whole modeling spectrum from feature analysis, deployment mapping, high-level design and down to implementation issues. To show that in spite of this ABS is not unwieldy, but rather easy to use and quite flexible, is the aim of the present tutorial.\n4 The Functional Layer 4.1 Algebraic Data Types The base layer of ABS is a simple language for parametric algebraic data types (ADTs) with a self-explaining syntax. The only predefined datatypes(Foot: There is one more predefined type that is used for synchronization which is explained in Sect. 6.) are Bool,Int, String, Unit and parametric lists as defined below. The type Unit is used as a type for methods without return value and works like Java’s void. All other types are user-defined. We assume that the Eclipse plugin is installed (see Sect. 1.3). To create a new ABS file in an existing ABS project, right click on the project in the explorer and choose New|ABS Module. In the input mask that pops up, specify a file name, for example, CustomerData, and click Finish. This creates a new file named CustomerData.abs in the workspace, which can be edited in the usual way. The running example of this tutorial has a banking theme. Let us create some datatypes related to customers. All type and constructor names must be upper-case.\ndata Level = Standard | Silver | Gold; data Customer = Test | Person(Int, Level) | Company(Int); There are three kind of customers defined by three different type constructors: a test customer, individual customers, and corporate customers. Individual customers are identified by a personal id and possess a status level while corporate customers are identified by their vat number. We can make this more explicit and, at the same, automatically create selector functions for the arguments of each type constructor by the following alternative definition:\ndata Customer = Test | Person(Int pid, Level) | Company(Int vat); Assume now that we want to define lists of customers. For this we can use the following built-in parametric list type, which provides a convenient concrete syntax for lists:\ndata List\u003cT\u003e = Nil | Cons(T, List\u003cT\u003e); List\u003cInt\u003e l = [1,2,3]; The definition of parametric lists demonstrates that type definitions may be recursive. Let us instantiate parametric lists with Customer and, at the same time, create a type synonym:\ntype CustomerList = List\u003cCustomer\u003e; Type synonyms do not add new types or functionality, but can greatly enhance readability.\n4.2 Functions The functional layer of ABS consists of a pure first-order functional language with definitions by case distinction and pattern matching. All function names must be lower-case. Let us begin by defining a function that computes the length of a list of customers:\ndef Int length(CustomerList list) = case list { Nil =\u003e 0 ; Cons(n, ls) =\u003e 1 + length(ls) ; _ =\u003e 0 ; } ; Several kinds of patterns are permitted on the left-hand side of case distinctions. In the example above, the first and second cases use a data constructor pattern. In the second case, this contains an unbound variable whose value is extracted and used on the right-hand side. The last case uses an underscore pattern containing an anonymous variable that matches anything. Naturally, it would have been possible to define a parametric version of Int length(List\u003cT\u003e list). This is left as an exercise to the reader. Here is another example illustrating the remaining patterns, that is, the literal pattern and the bound variable pattern:\ndef Int sign(Int n) = case n { 0 =\u003e 0 ; n =\u003e if (n \u003e 0) then 1 else -1 ; } ; The ABS parser does not attempt to establish whether case distinctions are exhaustive. If no pattern in a case expression matches, a runtime error results. It is up to the modeler to prevent this situation (in the near future, ABS will be equipped with the possibility of failure handling). Similarly, it is perfectly possible to define the following function:\ndef Int getPid(Customer c) = pid(c); However, if c has any other type than Person(Int,Level) at runtime, an error will result. We close this section by illustrating a piece of syntactic sugar for associative collection types such as sets, bags, sequences, etc. To construct concrete elements of such datatypes one typically needs to iterate several binary constructors, such as Insert(1,Insert(2,Insert(3,EmptySet))). This is cumbersome. The following idiom defines an n-ary constructor that uses concrete list syntax as its argument. By convention, the constructor should have the same name as the type it is derived from, but in lower-case.\ndata Set\u003cA\u003e = EmptySet | Insert(A, Set\u003cA\u003e); def Set\u003cA\u003e set\u003cA\u003e(List\u003cA\u003e l) = case l { Nil =\u003e EmptySet; Cons(hd, tl) =\u003e Insert(hd, set(tl)); } ; Errors are highlighted on the editor line where they occur as well as in the Problems tab of the messages subwindow\nSet\u003cInt\u003e s = set[1,2,3]; 4.3 Modules If you tried to type in the previous examples into the ABS Eclipse editor you got parser errors despite the definitions being syntactically correct (similarly as in Fig. 5). This is, because any ABS definition must be contained in exactly one module. ABS is equipped with a simple syntactic module system that is inspired by that of Haskell [33]. To make the examples of the previous section work, simply add a module declaration like this as the first line of the file:\nmodule CustomerData; Module names must be upper-case and define a syntactic scope until the end of the file or until the next module declaration, whatever comes first. Module names can also be part of qualified type names. Module declarations are followed by export and import directives. The former lists the types, type constructors, and functions that are visible to other modules, the latter lists the entities from other modules that can be used in the current module. With the type definitions of the previous section we might write:\nmodule CustomerData; export Standard, Customer, Company, getPid; ... module Test; import * from CustomerData; def Customer c1() = Company(2); def Customer c2() = Person(1,Standard); // erroneous The module CustomerData exposes three of its constructors and a function while module Test imports anything made available by the former. The definition of c1 is correct, but the definition of c2 gives a parse error about a constructor that cannot be resolved, because Person is not exported. The from clause constitutes an unqualified import. Instead, it is also possible to make qualified imports. For example, we could have written:\nimport CustomerData.Company, CustomerData.Customer; def CustomerData.Customer c1() = CustomerData.Company(2); In this case, however, one must also use qualified type names in the definitions as illustrated above. The ABS compiler knows one predefined module that does not need to be explicitly imported—the ABS standard library ABS.StdLib. It contains a number of standard collection types, such as lists, sets, maps, together with the usual functions defined on them. It also contains some other types and functions that are used often. The standard library module is contained in a file named abslang.abs. To look up the definition of any standard type or function (or any other type or function, for that matter), simply move the cursor over the identifier in question and press F3. For example, pressing F3 over the identifier Cons in the definition of length in the previous section opens a new tab that contains abslang.abs and jumps to the line that contains the definition of the constructor Cons. This lookup functionality is, of course, well-known to users of the Eclipse IDE.\n4.4 Abstract Data Types The module system allows to define abstract data types by hiding the type constructors. This implies that only functions can be used to access data elements. Their explicit representation is hidden. Of course, one then needs to supply suitable constructor functions, otherwise, no new elements can be created at all. In the example of the previous section we might decide to expose only the types and constructor functions as follows:\nmodule CustomerData; export Customer, Level, createCustomer, createLevel; def Customer createCustomer(Int id, String kind) = ... ; def Level createLevel() = ... ; We leave it as an exercise to write a suitable definition of createCustomer. As usual, the advantage of using abstract data types is that one can replace the definition of types without the need to change any client code.\n5 The OO-Imperative Layer 5.1 The Object Model ABS follows a strict programming to interfaces discipline [17]. This means that the only declaration types of objects are interface types. Consequentially, ABS classes do not give rise to type names. Apart from that, interface declarations are pretty standard and follow a Java-like syntax. They simply consist of a number of method signatures. Static fields are not permitted,(Foot: And neither are static classes and objects. Instead of static elements the ABS modeler should consider to use ADTs and functions.) but subinterfaces, even multiple subinterfaces, are permitted. Let us give an example that models the Customer type from previous sections in an object-oriented fashion:\nmodule CustomerIF; export Customer; import Level, createLevel from CustomerData; interface Customer { Int getId(); } interface IndvCustomer extends Customer {} interface CorpCustomer extends Customer { Level getLevel(); } As can be seen, interfaces (and also classes) can be exported. In fact, this is necessary, if anyone outside their modules is to use them. It is possible to mix object and data types: data types may occur anywhere within classes and interfaces as long as they are well-typed. Less obviously, reference types may also occur inside algebraic data types. As seen earlier, it is perfectly possible to declare the following type:\ntype CustomerList = List\u003cCustomer\u003e; Keep in mind, though, that it is not allowed to call methods in function definitions. The reason is that method calls might have side effects. It was mentioned already that classes do not provide type names. They are only used for object construction. As a consequence, in ABS it is always possible to decide when a class and when an interface name is expected. Therefore, interfaces and classes may have the same name. We do not recommend this, however, because it dilutes the programming to interfaces discipline. It is suggested to use a base name for the interface and derive class names by appending “Impl” or similar. A class may implement multiple interfaces. Class constructors are not declared explicitly, instead, class declarations are equipped with parameter declarations that implicitly define corresponding fields and a constructor. Class definitions then consist of field declarations, followed by an initialization block and method implementations. Any of these elements may be missing. Hence, we can continue the example as follows:\nclass CorpIndvCustomerImpl(Int id) implements IndvCustomer, CorpCustomer { Level lv = createLevel(); // no initialization block Level getLevel() { return lv; } Int getId() { return id; } } Here, the id field is modeled as a class parameter, because it is not possible to give a reasonable default value, which is otherwise required, because fields that have no reference type must be initialized. Reference type fields are initialized with null. In contrast to functions, method names need not (and cannot) be exported by modules. It is sufficient to get hold of an object in order to obtain access to the methods that are defined in its type. The most striking difference between ABS and mainstream OO languages is that in ABS there is no class inheritance and, therefore, also no code inheritance. So, how do we achieve code reuse? In ABS we decided to disentangle data design and functionality from the modeling of code variability. For the former, we use functions and objects (without code inheritance), whereas for the latter we use a layer on top of the core ABS language that permits to connect directly with feature models. This layer is discussed in Sect. 8. In a concurrent setting (see Sect. 6) one typically wants some objects to start their activity immediately after initialization. To achieve this in ABS, one can define a Unit run() method, which implicitly declares a class as active and lets objects execute the code in the body of the run method after initialization. Classes without a run() method are called passive and their objects react only to incoming calls.\n5.2 The Imperative Layer ABS has standard statements for sequential composition, assignment, while-loops, conditionals, synchronous method calls, and method return. To illustrate all of these, one can look at the implementation of method findCustomer( CustomerList) in class CorpIndvCustomerImpl (don’t forget to add it to the implemented interfaces as well to render it visible!).\nCustomer findCustomer(CustomerList cl) { Customer result; Int i = 0; while (i\u003clength(cl)) { Customer curCust = nth(cl,i); Int curId = curCust.getId(); if (id==curId) {result = curCust;} } return result; } In addition to the various constructs, we can illustrate several ABS-specific restrictions: it is necessary that the final statement in the method body is a return statement with the correct type. A typical ABS idiom is, therefore, to declare a local result variable. Neither for-loops nor breaks from loops are supported at the moment. To avoid going through the remaining list after the element has been found, one would need to add and test for a Bool found variable. Complex expressions are not allowed at the moment in tests of conditionals or loops. The workaround, as shown here, is to declare a local variable that holds an intermediate result. While these restrictions can be slightly annoying they hardly matter very much. It is likely that some of them will be lifted in the future, once it is better known what modelers wish. A more fundamental restriction concerns the usage of fields in assignment statements: assignments to fields and field lookups are only possible for the current object. Given a field f, an assignment of the form x = f; is always implicitly qualified as x = this.f; and an assignment of the form f = exp; is always implicitly qualified as this.f = exp;. This implies that fields in ABS are object private. They cannot be directly seen or be modified by other objects, not even by objects from the same class (as is possible even for private fields in Java). In other words, ABS enforces strong encapsulation of objects: it is only possible to view or change the state of another object via getter- and setter-methods. For example, it is not possible to change the second line in the body of the while-loop of findCustomer(CustomerList) as follows:\nInt curId = curCust.id; The designers of ABS consider object encapsulation not as a restriction, but as a virtue: it makes all cross references between objects syntactically explicit. This avoids errors that can be hard to find. In addition it makes static analysis much more efficient, because any cross reference and possible side effect to a different object can be associated with a unique method contract. For the practicing ABS modeler object encapsulation is greatly alleviated by the method completion feature of the Eclipse editor: if one types the beginning of the example above “Int curId = curCust.”, then a pop-up menu will offer a selection of all methods that are known for objects of type Customer, the required getter-method getId() among them. If a suitable method is not found, then the modeler can take this as a hint that it needs to be implemented or added to the interface. ABS is a block-structured language. Blocks are delimited by curly braces (no semicolon afterward) and may appear at four different places in a program:\nas a way to group several statements and provide a scope for local variables–blocks are necessary for bodies of loops and conditionals that have more than one statement; as method bodies; as the (optional) class initialization block, between field and method declarations; as an (optional) implicit “main” method at end of a module. The last usage serves as an entry point for execution of ABS programs. At least one main block in one module is necessary for executing an ABS project, otherwise it is not clear which objects are to be created and executed. Any module that has a main block is selectable as an execution target via the Eclipse Run Configurations ... dialog or simply by right clicking on the desired module in the explorer and selection of Run As. We might complete the example by specifying the following main block for module CustomerIF:\n{ Customer c = new CorpIndvCustomerImpl(17); // create some customers Customer d = new CorpIndvCustomerImpl(16); CustomerList l = Cons(c,Cons(d,Nil)); // create list of customers Customer e = c.findCustomer(l); // we should find c in l } This code illustrates at the same time the usage of the new statement, which works as in Java. As usual in Eclipse, pressing the F4 key displays the type hierarchy pertaining to a class or interface name at the cursor position.\n6 The Concurrency Layers 6.1 Background One of the most distinctive features of ABS is its concurrency model. If we look at commercial programming languages such as C, C++, or Java, one can observe that, despite intense efforts in the last decade, none of them has a fully formalized concurrency model. Even though there are promising efforts towards a formal concurrency model of Java [5], the details are so complex that they are likely to compromise usability of any resulting system. The reason is that current industrial programming languages have a very low-level concurrency model and do not natively support distributed computation. This has practical consequences, such as burdening the programmer with, for example, prevention of data races. A more fundamental problem is the impossibility to design a compositional proof system for such languages. By compositionality we mean that one can specify and verify the behavior of a single method in isolation from the rest of the system. This is a prerequisite for being able to deduce global behavior from the composition of local behavior. In a setting, where concurrent objects can arbitrarily cross-reference each other, this is hardly possible.\nArbitrarily complex, global invariants, might be needed to describe behavior. One approach to tackle the problem is to impose structure on concurrent objects and to make their dependencies syntactically explicit. In the realm of Java, JCoBox [39] is a suitable framework. It has been simplified and renamed into Concurrent Object Group (COG) in the context of ABS. COGs constitute the lower tier of the ABS concurrency model and are intended for closely cooperating concurrent tasks. A second shortcoming of mainstream programming languages is the lack of support for distributed computation, that is, asynchronous communication among nodes that do not share memory. This form of concurrency has been abstracted into the Actor model [23] and is realized with first-class support in recent languages such as Scala. ABS implements a version of Actor-based distributed computation where COGs form the primitive units of distribution. This constitutes the upper tier of the ABS concurrency model. Its main ideas are derived from the modeling language Creol [26].\n6.2 Component Object Groups An ABS Concurrent Object Group (COG) is a collection of tasks with shared memory and processor. This means that exactly one task is active at any given time and tasks can cross-reference each other. The situation can be visualized as in Fig. 6. Within a COG, synchronous as well as asynchronous method calls are permitted. For the former, we use the standard syntax target.method(arg1,arg2,...). Synchronous method calls within COGs represent sequential execution of code, that is, they block the caller and execute the code of the target until control is returned. Asynchronous method calls use the syntax target!method(arg1,arg2,...) and they cause the creation of a new task that is to execute the code of the target. Unlike in synchronous calls, execution of the code of the caller continues. The main point to understand about COGs is that multitasking is not preemptive (decided by a scheduler). Rather it is an explicit decision of the ABS modeler when control is transferred to another task. To this end, ABS provides scheduling statements that allow cooperative multitasking. In between the explicit scheduling points, only one task is active, signified by the (single) lock of a COG being set to \u0026#8868. As a consequence, data races between synchronization points simply cannot happen, which was an important design goal of ABS.\n6.3 Scheduling and Synchronization So, how are scheduling points specified in ABS? It is here that we encounter a second, central concurrency principle of ABS: communication and synchronization are decoupled. This is done via future types [12]. For any ABS type T a legal type name is Fut\u003cT\u003e and one can assign to it the result of any asynchronous method call with return type T. A variable declared with type Fut\u003cT\u003e serves as a reference to the future result of an asynchronous call and allows to retrieve it once it will have been computed. For example, the final line of the example on p. 15 can be rewritten to:\nFut\u003cCustomer\u003e e = c!findCustomer(l); // do something else ... Now the call creates a new task in the current COG and declares e as a future reference to its final result. The following code is executed immediately. The future mechanism allows to dispatch asynchronous calls, continue with the execution, and then synchronize on the result, whenever it is needed. Synchronization is achieved by the command await g, where g is a polling guard. A guard is a conjunction of either side-effect free boolean expressions or future guards of the form f?. In the latter, f is a variable that has a future type. If the result to which f? is a reference is ready and available, then the expression evaluates to true. When the guard of an await statement evaluates to true, the computation simply continues. If, however, a guard is not true, then the current task releases the lock of its COG and gives another task in that COG the chance to continue. When later the task is scheduled gain, the guard is re-evaluated, and so on, until it finally becomes true. We call this a conditional scheduling point or conditional release point. To continue the previous example we could write:\nawait e?; If the asynchronous call to findCustomer(l) has finished, then execution simply continues. Otherwise, the lock of the current COG is set to ⊥ and the processor is free to proceed with another task. For efficiency reasons ABS allows only monotonic guards and only conjunctive composition. Once the result from an asynchronous call is available, it can be retrieved with a get-expression that has a future variable as its argument. In the example this may look as follows:\nCustomer f = e.get; In summary, the following programming idiom for asynchronous calls and retrieving their results is common in ABS:\nFut\u003cT\u003e v = o!m(e); ... ; await v?; r = v.get; ABS does not attempt to check that each get expression is guarded by an await statement. So what happens when the result of an asynchronous call is not ready when get is executed? The answer is that the execution of the COG blocks. The difference between suspension and blocking is that in the latter case no task in same COG can continue until the blocking future is resolved. Sometimes it is convenient to create an unconditional scheduling point, for example, to insert release points into long running sequential tasks. The syntax for unconditional scheduling statements in ABS is “suspend;”.\n6.4 Object and COG Creation In the previous section we discussed the fundamental concurrency model of ABS, which is based on COGs. Whenever we create an object with the new statement, it is by default created in the same COG as the current task (see upper part of Fig. 7). This is not adequate for modeling distributed computing, where each node has its own computing resources (processor) and nodes are loosely coupled. In an ABS model of a distributed scenario we associate one COG with each node. New COGs are implicitly created when specifying the cog keyword at object creation (see lower part of Fig. 7): this creates a new COG and places the new object inside it. At the moment, COGs are not first-class objects in ABS and are accessible only implicitly through their objects.(Foot: There is an extension for ABS runtime objects that allows explicit and dynamic grouping of COGs [28].) As a consequence, it is not possible to re-enter via recursive calls into the same execution thread. This is the reason why a simple binary lock for each COG is sufficient. Let us extend our running example with an Account class and COG creation:\nmodule Account; interface Account { Int getAid(); Int deposit(Int x); Int withdraw(Int x); } class AccountImpl(Int aid, Int balance, Customer owner) implements Account { ... } { [Near] Customer c = new CorpIndvCustomerImpl(3); [Far] Account a = new cog AccountImpl(1,0,c); Fut\u003cInt\u003e dep = a!deposit(17); Fut\u003cInt\u003e with = a!withdraw(17); await dep? \u0026 with?; Int x = dep.get; Int y = with.get; Int net = x + y; } We create an account objects in a different COG from the current one. Note that there is no sharing of objects between COGs, so that the variable c provides no alias to the object parameter c in the constructor AccountImpl(1,0,c). The tasks resulting from the two asynchronous calls will be executed on the same node, which is different from the current one. A conjunctive guard ensures that the retrieval of the results is safe. It is possible to visualize the execution of ABS code in two ways. To start the graphical ABS Debugger, simply right click on the file with the Account module in the explorer and select Run As|ABS Java Backend (Debug). This will automatically switch to the ABS Debug Perspective (see Fig. 8) and start the Eclipse debugger.\nAll the usual features of a graphical debugger are available: navigation, breakpoints, state inspection, etc. If instead, the backend Run As|ABS Java Backend (Debug with Sequence Diagram) is chosen, then in addition a UML sequence diagram that has a lifeline for each created COG is created and dynamically updated after each debugger step, see Fig. 9. Synchronous method calls to targets not in the current COG make no sense and are forbidden. For example, if we replace one of the asynchronous calls above with a.deposit(17), a runtime error results. One possibility to avoid this is to annotate declarations with one of the types Near or Far, as shown above. This tells the compiler that, for example, a is in a different COG and cannot be the target of a synchronous call. Obviously, it is tedious to annotate all declarations; moreover, the annotations tend to clutter the models. To address this problem, ABS implements a far/near analysis, which automatically infers a safely approximated (in case of doubt, use “far”) location type [41]. The inferred types are displayed in the Eclipse editor as superscripts (“N” for near, “F” for far) above the declared types. All annotations in the example can be inferred automatically: simply delete the annotations to see it. It is also possible to annotate a declaration with Somewhere, which overrides the type inference mechanism and tells the compiler not to make any assumptions. Default is the annotation Infer, but this can be changed in the ABS project properties. It is entirely possible that execution of an ABS model results in a deadlock during runtime, as is exemplified by the model in Fig. 10. Objects c, e and d are in different COGs, say cog_c and cog_d . The task that executes m1 is in cog_c while the task executing m2 is put into the second COG cog_d . During this execution m3 is called on e, which is located in the first COG cog_c . For m3 to proceed it needs to obtain the lock of cog_c , but this is not possible, because m1 still waits for the result of m2. Hence, neither COG can progress. Deadlocks are very difficult to avoid in general. Deadlock-free concurrent languages tend to be too restrictive to be usable and, unlike data race-freeness, are not a practical option.\nclass C { C m1(C b, C c) { Fut\u003cC\u003e r = b!m2(c); return r.get; } C m2(C c) { Fut\u003cC\u003e r = c!m3(); return r.get; } C m3() { return new C(); } } { C c = new C(); C d = new cog C(); C e = new C(); c!m1(d,e); } Fig. 10. Example for deadlock in ABS\nIn ABS many deadlocks can be avoided by supplying enough release points. In the example above it is sufficient to guard one of the get expressions. In addition, there is an automatic deadlock analysis for ABS [18] that is currently being implemented.\n6.5 Formal Semantics of Concurrent ABS The ABS language has a mathematically rigorous, SOS-style semantics [13, 25]. This tutorial introduction is not the place go into the details, but we sketch the main ideas. The central issue is to give an appropriate structure to the terms that represent ABS runtime configurations. They are collections over the following items:\nCOGs are identified simply by a name b for their lock whose value can be either ⊤ or ⊥. Objects have a name o, need to have a reference to their COG b, to their class C, and they also have a local state σ that holds the current field values. Tasks have a name n, a reference to their COG b and to the object o whose code they are executing. They also have a state σ withe values of local variables and a program counter s that gives the next executable instruction. Task names n also double as futures, because they contain exactly the required information. A runtime configuration may consist of any number of the above items. The operational semantics of ABS is given by rewrite rules that match the next executable statement of a task (and thereby also the current COG and object). A typical example is the rewrite rule that realizes creation of a new COG:\nwhere:\n\\(b’, o’, n’\\) new;\n\\(\\overline{T f}; s’\\) init block of class \\(C\\) and \\(\\sigma’_{init}\\) binds constructor parameters \\(v’\\);\n\\(\\sigma’_{init} = \\overline{T f}\\);\n\\(s_{task} = s’\\{\\mathbf{this}\\, / o’;\\mathbf{suspend}\\}\\).\nThe rule matches a new cog statement in task \\(n\\), COG \\(b\\), current object \\(o\\), and subsequent statements s. First we need to create a new COG with a fresh name \\(b’\\) and a new object \\(o’\\) of class \\(C\\). The new COG starts immediately to execute the initialization code of its class \\(C\\) in a new task \\(n’\\), therefore, the lock of \\(b’\\) is set to ⊤. Note that the current object this must be instantiated now to the actual object \\(o’\\). After initialization, execution is suspended. The original task \\(n\\) immediately continues to execute the remaining code s as there is no release point here. The value of the object reference z is replaced with the new object \\(o’\\).\n7 Extensions 7.1 Pluggable Type System All declarations (fields, methods, classes, interfaces) in ABS can carry annotations. These are simply expressions that are enclosed in square brackets. The location type system in Sect. 6.4 provided examples. Other annotations can be logical expressions that are used as assertions, contracts, or invariants during verification or runtime assertion checking. This goes beyond this tutorial. The location types are a so-called pluggable type system. Such type systems can be realized easily in ABS via meta annotations. The special annotation [TypeAnnotation] declares the data type definition immediately following it to be a definition for type annotations and makes the parser aware of it. For example, the location type system is declared as follows:\n[TypeAnnotation] data LocationType = Far | Near | Somewhere | Infer; // usage [LocationType: Near] T n; 7.2 Foreign Language Interface As a modeling language ABS does not contain mechanisms for I/O, because these are typically implementation-dependent. Of course, one often would like to have some output from the execution of an ABS model. This is possible with a general foreign language interface (FLI) mechanism that not only can be used to implement I/O for ABS, but to connect ABS models with legacy code in implementation languages in general. At the moment, the ABS FLI is realized for the Java language. An ABS class that is to be implemented in Java needs three ingredients:\nimport of helper functions and classes from the module ABS.FLI; declaration as being foreign by the annotation [Foreign]; default ABS implementations of all interface methods. A simple example can look as follows:\nimport * from ABS.FLI; interface Hello { String hello(String msg); } [Foreign] class HelloImpl implements Hello { String hello(String msg) { return \"default implementation\"; } } { Hello h = new HelloImpl(); h.hello(\"Hi there\"); } The default implementation is used for simulation of ABS code without Java. It is now possible to implement a Java version of the HelloImpl class in a Java project and to connect that project with ABS. The details of how this is done are explained at the HATS tools site. Basically, one extends the Java class HelloImpl_c that was generated by the ABS Java backend with a new implementation of the Java method hello(String). By convention, the Java methods carry the prefix fli.\nimport abs.backend.java.lib.types.ABSString; import abs.backend.java.lib.runtime.FLIHelper; import Test.HelloImpl_c; public class HelloImpl_fli extends HelloImpl_c { @Override public ABSString fli_hello(ABSString msg) { FLIHelper.println(\"I got \"+msg.getString()+\" from ABS\"); return ABSString.fromString(\"Hello ABS, this is Java\"); } } On the Java side any Java construct can be used. ABS provides a Java package abs.backend.java.lib.types containing declarations of the built-in ABS types usable in Java such as ABSString. Execution of the ABS main block above will now cause the Java output “I got Hi there from ABS” to be printed on the system console.\n8 Product Line Modeling with ABS 8.1 Product Line Engineering One of the aims of ABS is to provide a uniform and formal framework for product line engineering (PLE) [35], a practically highly successful software reuse methodology. In PLE one distinguishes two separate development phases (see Fig. 11). During family engineering one attempts to distill the commonality among different products into a set of reusable artifacts. At the same time, the variability of the product line is carefully planned. This is typically done in a feature-driven manner, and the relation of features, as well as constraints in their combination is documented in a feature model with the help of feature description languages [40]. In the application engineering phase, individual products are being built by selecting features and by combining the artifacts that implement them in a suitable way. One drawback of current practice in PLE is that feature description languages make no formal connection between features and their implementation. This renders products assembly ad hoc and error-prone. That issue is addressed in ABS with language extensions for modeling of features, for connecting features to their realization, as well as for feature selection and product specification [10]. In this section we introduce the PLE extensions of ABS. A fuller discussion of various approaches to achieve greater flexibility in object-oriented modeling is contained in the chapter by Clarke in this volume [8]. If one wants to maintain a connection between features and code, then the central issue are the mechanisms being used to compose the code corresponding to new features with the existing code. In current practice, this is often done by “glue code” written in scripting languages. ABS has the ambition that models can be statically analyzed. This means that the feature composition mechanism must be well-structured and represent a suitable match for the analysis methods used in ABS [14].\nSuch a mechanism is delta-oriented programming (DOP) [36, 38], because it allows to modify object-oriented code in a structured manner at the granularity of fields and methods, which is adequate for the contract-based specification approach in ABS [21]. To summarize, the ABS-extensions used to model product lines consist of four elements [9, 10], which we describe now in turn:\nA feature description language A language for deltas that modify ABS models A configuration language connecting features with the deltas that realize them A language for product configuration 8.2 Feature Description Modern software development processes, notably agile processes and PLE, tend to be feature-driven. A number of mature and useful formalisms for feature description have been developed in the last decade. For ABS we use a slight modification of the textual variability language (TVL) [11], which has the advantage of having a formal semantics and a textual representation. The feature description language used in ABS is called μTVL and differs from TVL in that (i) attribute types that are not needed are omitted and (ii) the possibility to have multiple root features. These are useful to model orthogonal variability in product lines. Let us build a product line based on the Account interface from Sect. 6.4. Assume we want to distinguish between checking and saving accounts. The latter may pay interest, whereas the former usually don’t. Optionally, a checking account (but not a saving account) may permit an overdraft or incur fees for transactions. A graphical representation of the Account feature model is in Fig. 12. The textual rendering in μTVL looks as follows:\nroot Account { group allof { Type { group oneof { Check {ifin: Type.i == 0;}, Save {ifin: Type.i \u003e 0; exclude: Overdraft;} } Int i; // interest rate }, opt Fee {Int amount in [0..5];}, opt Overdraft } } In μTVL one represents each subhierarchy in the feature tree by a group of features, which can be further qualified as inclusive (allof) or alternative (oneof). Within a group there is a comma-separated list of feature declarations. Each feature declaration may be optional (opt) and have restrictions (ifin:), exclusions (exclude:), or requirements (include:). Feature parameters are declared after the declaration of a subhierarchy. A feature model appears in a separate file with extension .abs. The Eclipse editor supports syntax and parse error highlighting. There can be several feature files with feature declarations. These are interpreted as orthogonal feature hierarchies that are all part of the same feature model. The semantics of feature models is straightforward by translation into a boolean/integer constraint formula, see [10, 11]. For example, the feature model above is characterized by the following formula: 0 ≤ Account ≤ 1 ∧ Type → Account ∧ Overdraft† → Account ∧ Fee† → Account ∧ Type + Fee† + Overdraft† = 3 ∧ 0 ≤ Type ≤ 1 ∧ Check → Type ∧ Save → Type ∧ Save → ¬Overdraft ∧ Check + Save = 1 ∧ 0 ≤ Check ≤ 1 ∧ 0 ≤ Save ≤ 1 ∧ 0 ≤ Fee† ≤ 1 ∧ 0 ≤ Overdraft† ≤ 1 ∧ Fee → Fee† ∧ Overdraft → Overdraft† ∧ 0 ≤ Save ≤ 1 ∧ 0 ≤ Check ≤ 1 ∧ Fee → (Fee.amount \u003e= 0 ∧ Fee.amount \u003c= 5) ∧ Check → (Type.i = 0) ∧ Save → (Type.i \u003e 0). It is easy to check validity of a given feature selection for a feature model F : for any selected feature f and parameter value p := v one simply adds f = 1 ∧ p = v to the semantics of F and checks for satisfiability with a constraint solver. The constraint solver of ABS can:\nfind all possible solutions for a given feature model and check whether a feature selection is a solution of a feature model. The latter check is performed implicitly in the ABS Eclipse plugin, whenever the user requests to build a product based on a specific feature selection (see Sect. 8.5).\n8.3 Delta Modeling As mentioned above, the realization of features in ABS is done with delta modules (or deltas, for short), a variant of delta-oriented programming (DOP). This constitutes the main reuse principle of ABS and replaces other mechanisms such as code inheritance, traits, or mixins. In delta modeling we assume that one outcome of the family engineering phase (see Fig. 11) is a core or base product with minimal functionality. Product variants with additional features are obtained from it by applying one or more deltas that realize the desired features, as illustrated in Fig. 13. In ABS, deltas have the following capabilities:\nDelta modules may add, remove or modify classes and interfaces Permitted class modifications are: adding and removal of fields adding, removal and modification of methods extending the list of implemented interfaces The actual reuse mechanism is located in the modification of methods: the description of a method modification in a delta can access the most recent incarnation of that method in a previous delta by the statement original(...);. This will cause the compiler to insert the body of the referred method at the time when the deltas are applied. The signature of original() must be identical to the one of the modified method. The compiler checks the applicability of deltas and ensures well-typedness of the resulting code. It is because of this reuse mechanism that once can say that the granularity of delta application is at the level of methods. There is a certain analogy between original() in DOP and super()-calls in OO languages with code inheritance. The crucial difference is that original() references are resolved at compile time (product build time), while super()-calls occur at runtime. As a consequence, there is a runtime penalty for the latter. Assume we have the following implementation of the withdraw(Int) method of the Account interface, which ensures that we cannot withdraw more than the current balance:\nclass AccountImpl(Int aid, Int balance, Customer owner) implements Account { Int withdraw(Int x) { if (balance - x \u003e= 0) { balance = balance - x; } return balance; } } Now we would like to create a delta module that realizes the feature Fee. We need to modify withdraw(Int), which can be achieved by the following delta:\ndelta DFee(Int fee); // Implements feature Fee uses Account; modifies class AccountImpl { modifies Int withdraw(Int x) { Int result = x; if (x\u003e=fee) result = original(x+fee); return result; } } One or more features can be put into a file with extension .abs. The connection between different deltas and a base implementation is given via the uses clause that refers to the module where the base is found. Like classes, deltas can have parameters, however, these are not fields, but are instantiated at product build time. Normally, there is a correspondence between the parameters of deltas and those of the features they are supposed to implement. The modified withdraw(Int) method is implemented by a suitable call to the original version after a check that the withdrawn amount is not trivially small. We must declare a result variable to ensure that the return statement is last. Assume further we want to realize the Save feature. One must ensure that the interest rate is set to 0. ABS deltas at this time do not support to add or modify class initialization blocks. To change the initial value of a field, we simply remove the field declaration and add it again with a suitable initial value:\ndelta DSave(Int i); // Implements feature Save uses Account; modifies class AccountImpl { removes Int interest; adds Int interest = i; } Of course, we assume here that the interest field has been added in the first place in the earlier delta DType. This requires to specify and check temporal constraints on the application of deltas as we shall see in the following section. Application of a concrete delta is illustrated with DSave in Fig. 14. Syntax and parse error highlighting for delta modules works as usual. Automatic completion works as well, but it is only done relative to the base product.\nThe reason is that before product build time, the compiler cannot know which deltas have been applied before. For the same reason, only a limited amount of type checking is done. Research to lift type checking to the family level is under way [29, 37].\n8.4 Product Line Configuration So far, we have two models relating to product lines: the feature model and the delta model, that is, the feature implementation. Unlike any other formalism we are aware of, in ABS we can make a formal connection between these. This is the key to being able to analyze whole product lines and not merely individual products. In ABS, the connection between features and their realization (illustrated in Fig. 15) is done in a dedicated product line configuration file. This makes debugging easy, because all information about the realization of a given feature model is collected in one place. To establish a connection between features and deltas, the configuration files need to specify three things:\nthey must associate features with their implementing delta modules by application conditions; they need to resolve conflicts in the application order by giving partial temporal constraints on delta application; they need to pass the attribute values of features to the parameters of the delta modules. We can illustrate all three aspects with our running example. The following file (again, use file extension .abs) defines a product line named Accounts based on the five features of the feature model in Fig. 12.\nproductline Accounts; features Type, Fee, Overdraft, Check, Save; delta DType (Type.i) when Type; delta DFee (Fee.amount) when Fee; delta DOverdraft after DCheck when Overdraft; delta DSave (Type.i) after DType when Save; delta DCheck after DType when Check; For each delta that is to be used for implementing any of the features one specifies:\nthe application conditions (when clauses), that is, the feature(s) that are being realized by each delta and whose presence triggers delta application; the delta parameters which are derived from feature attribute values; a strict partial order of delta application (after clauses) to ensure well-definedness of delta applications and resolve conflicts. In the example, there is a one-to-one correspondence between deltas and features, which is reflected in the application conditions. Likewise, the feature attributes Type.i and Fee.amount directly can be used as parameters of the corresponding deltas. The temporal constraints of DSave and DCheck ensure that the field interest is present. The constraint of DOverdraft makes sure that this delta is only applied to checking accounts. It would also have been possible to express this constraint at the level of the feature model with an includes: clause. It is up to the modeler to decide whether a given constraint is a property of the feature model or of the product line.\n8.5 Product Selection The final step in PLE with ABS is product selection. Whereas the activities that took place until now can be viewed as mostly being part of family engineering, the selection process is always part of application engineering.\nTo create a product it is sufficient to list the features that should be realized in it and to instantiate the feature attributes with concrete values. The syntax is very simple and self-explaining. As any other ABS file, product selection files have the .abs extension and there is Eclipse support for syntax and parse error highlighting. Some examples for the Accounts product line are as follows:\nproduct CheckingAccount (Type{i=0},Check); product AccountWithFee (Type{i=0},Check,Fee{amount=1}); product AccountWithOverdraft (Type{i=0},Check,Overdraft); product SavingWithOverdraft (Type{i=1},Save,Overdraft); The simplest product that can be built is CheckingAccount. The second product above extends it by charging a fee of one unit per transaction. The ABS compiler uses the product selection file and the other related files to create a “flattened” ABS model where all deltas have been applied such that it contains only core ABS code. In a first step, the compiler checks that the product selection is valid for the given feature model as described in Sect. 8.2. It then uses the product line configuration file to decide which deltas need to be applied and how they are instantiated. The partial order on the deltas is linearized. It is up to the modeller to ensure (possibly, by adding temporal constraints) that different linearizations do not lead to conflicting results. Finally, the resulting core ABS model is type-checked and compiled to one of the ABS backends in the standard way. As all parts of the ABS language the product line modeling languages have a formal semantics—the details are found in [10]. Different products can be selected in the Run|Run Configurations ... dialog from the ABS Product menu. Invalid product selections or type errors in the configuration files will be displayed at this stage. For example, selection of the SavingWithOverdraft product above results in an error, because the constraints in the feature model are not satisfied.\nAfter selection of a valid product one can run and debug the resulting core ABS model as described earlier. The ABS compiler additionally creates always as base product that corresponds to the given ABS model without any features or deltas. This product appears under the name \u003cbase\u003e in the product selection menu. If we execute the main class of the Account module in Sect. 6.4 in the base product, we obtain the result 37 in the variable net, whereas if we run the product AccountWithFee, we obtain 34. A current limitation of the Eclipse ABS plugin is that the debugger correctly displays the runtime configuration and the values of variables of products, but in the editor window only the core product is displayed.\n9 Concluding Remarks In this tutorial we gave an introduction to the abstract modeling language ABS. Uniquely among current modeling languages, ABS has a formal semantics and covers the whole spectrum from feature modeling to the generation of executable code in Java. Development of ABS models is supported by an Eclipse plugin. A very important point is that ABS offers a wide variety of modeling options in a uniform, homogeneous framework, see Fig. 17. This allows to select an appropriate modeling style for each modeled artifact. It also supports rapid prototyping and design-time analysis, because ADT-based models can be refined later (dashed arrow). Of course, as any other formalism, ABS has also limitations: it is not suitable to model low-level, thread-based concurrency with shared data. Hence, ABS is not suitable to model multi-core applications or system libraries. In this sense, approaches such as [5] are complementary to ABS. As mentioned earlier, the analysis capabilities and the ABS runtime component layer are beyond this tutorial, but some chapters in this volume cover part of the material.\nAcknowledgments The development and implementation of ABS was a collaborative effort of the many researchers involved in the HATS project. While the text of this tutorial has been written from scratch by the author, it could never have been done without the background of all the papers, presentations, and discussions provided by many colleagues. Special thanks go to the main contributors to Work Package 8: Frank de Boer, Einar Broch Johnsen, and Ina Schaefer.\nFurther Reading This paper is a tutorial on ABS and not a language specification nor a formal definition. A more technical and more detailed description of ABS and its tool set is contained in the paper trio [10, 20, 25]. The most detailed document about ABS that also contains a formal semantics is [13]. The official ABS Language Specification is [2]. Finally, for several case studies done with ABS, please look here [15]. It is stressed at several places in this tutorial that ABS has been designed with the goal of permitting automatic static analyses of various kinds. This tutorial concentrates on the ABS language and its development environment. In the paper by Albert in this volume [4] automated resource analysis for ABS is explained in detail. Information on deadlock analysis and formal verification of ABS can be found in [14]. The chapter by Poetzsch-Heffter in this volume [34] contains a general discussion of verification of concurrent open systems.",
    "description": "This tutorial gives an overview of the ABS language.",
    "tags": [],
    "title": "Language Tutorial",
    "uri": "/documentation/tutorials/language-tutorial/index.html"
  },
  {
    "breadcrumb": "The ABS Language \u003e Getting Started",
    "content": "The collaboratory is a browser-based development environment for ABS. It integrates an editor, the syntax checker and simulator, and the SACO resource analysis tool.\nRunning the Collaboratory using Docker To run the collaboratory, first install docker from https://www.docker.com. Then, run the following command in a terminal window:\ndocker run -d --rm -p 8080:80 --name collaboratory abslang/collaboratory:latest When the command has finished, connect a browser to http://localhost:8080 and start using ABS!\nTo stop the collaboratory, use the following command:\ndocker stop collaboratory",
    "description": "The collaboratory is a browser-based development environment for ABS.  It integrates an editor, the syntax checker and simulator, and the SACO resource analysis tool.",
    "tags": [],
    "title": "Running a Browser-Based IDE",
    "uri": "/getting_started/docker/index.html"
  },
  {
    "breadcrumb": "The ABS Language",
    "content": "There are various ways of running ABS models.\nUse On-Line Tools The simplest way to use the ABS tools is on-line, in the collaboratory. This means you only need a modern browser to start experimenting with ABS. The tools work best with Firefox and Chrome.\nAn introduction and link to the collaboratory can be found at http://abs-models.org/laboratory/.\nInstalling Command-Line ToolsMany of the tools can be run from the command line. This page describes how to run various tools on a local machine.\nRunning a Browser-Based IDEThe collaboratory is a browser-based development environment for ABS. It integrates an editor, the syntax checker and simulator, and the SACO resource analysis tool.\nInstalling Editor SupportWe provide support for Emacs, Atom and Visual Studio Code.",
    "description": "There are various ways of running ABS models.\nUse On-Line Tools The simplest way to use the ABS tools is on-line, in the collaboratory. This means you only need a modern browser to start experimenting with ABS. The tools work best with Firefox and Chrome.\nAn introduction and link to the collaboratory can be found at http://abs-models.org/laboratory/.\nInstalling Command-Line ToolsMany of the tools can be run from the command line. This page describes how to run various tools on a local machine.",
    "tags": [],
    "title": "Getting Started",
    "uri": "/getting_started/index.html"
  },
  {
    "breadcrumb": "The ABS Language \u003e Documentation \u003e Tutorials",
    "content": "Core ABS ABS is a modeling language which combines functional and imperative programming styles to develop high-level executable models. Concurrent object groups execute in parallel and communicate through asynchronous method calls. To intuitively capture internal computation inside a method, we use a simple functional language based on user-defined algebraic data types and functions. Thus, the modeler may abstract from the details of low-level imperative implementations of data structures, and still maintain an overall object-oriented design which is close to the target system. At a high level of abstraction, concurrent object groups typically consist of a single concurrent object; other objects may be introduced into a group as required to give some of the algebraic data structures an explicit imperative representation in the model. In this tutorial, we aim at high-level models and the groups will consist of single concurrent objects. The functional sublanguage of ABS consists of a library of algebraic data types such as the empty type Unit, booleans Bool, integers Int, parametric data types such as sets Set\u003cA\u003e and maps Map\u003cA\u003e (given a value for the type variable A), and (parametric) functions over values of these data types. For example, we can define polymorphic sets using a type variable A and two constructors EmptySet and Insert, and a function contains which checks whether an element el is in a set ss recursively by pattern matching over ss:\ndata Set\u003cA\u003e = EmptySet | Insert(A, Set\u003cA\u003e); def Bool contains\u003cA\u003e(Set\u003cA\u003e ss, A el) = case ss { EmptySet =\u003e False ; Insert(el, _) =\u003e True; Insert(_, xs) =\u003e contains(xs, el); }; Here, the cases p=\u003eexp are evaluated in the listed order, underscore works as a wild card in the pattern p, and variables in p are bound in the expression exp. The imperative sublanguage of ABS addresses concurrency, communication, and synchronization at the concurrent object level in the system design, and defines interfaces and methods with a Java-like syntax. ABS objects are active; i.e., their run method, if defined, gets called upon creation. Statements are standard for sequential composition s1;s2, assignments x=rhs, and for the skip, if, while, and return constructs. The statement suspend unconditionally suspends the execution of the active process of an object by adding this process to the queue, from which an enabled process is then selected for execution. In await g, the guard g controls the suspension of the active process and consists of Boolean conditions b and return tests x? (see below). Just like functional expressions e, guards g are side-effect free. If g evaluates to False, the active process is suspended, i.e., added to the queue, and some other process from the queue may execute. Expressions rhs include the creation of an object group new C(e), object creation in the group of the creator new local C(e), method calls o!m(e) and o.m(e), future dereferencing x.get, and pure expressions e apply functions from the functional sublanguage to state variables. Communication and synchronization are decoupled in ABS. Communication is based on asynchronous method calls, denoted by assignments f=o!m(e) to future variables f. Here, o is an object expression and e are (data value or object) expressions providing actual parameter values for the method invocation. (Local calls are written this!m(e).) After calling f=o!m(e), the future variable f refers to the return value of the call and the caller may proceed with its execution without blocking on the method reply. There are two operations on future variables, which control synchronization in ABS. First, the guard await f? suspends the active process unless a return to the call associated with f has arrived, allowing other processes in the object group to execute. Second, the return value is retrieved by the expression f.get, which blocks all execution in the object until the return value is available. The statement sequence x=o!m(e);v=x.get encodes commonly used blocking calls, abbreviated v=o.m(e) (often referred to as synchronous calls). If the return value of a call is without interest, the call may occur directly as a statement o!m(e) with no associated future variable. This corresponds to message passing in the sense that there is no synchronization associated with the call.\nReal-Time ABS Real-Time ABS is an extension of ABS which captures the timed behavior of ABS models. An ABS model is a model in Real-Time ABS in which execution takes zero time; thus, standard statements in ABS are assumed to execute in zero time. Timing aspects may be added incrementally to an untimed behavioral model. Our approach extends the distributed concurrent object groups in ABS with an integration of both explicit and implicit time.\nDeadlines The object-oriented perspective on timed behavior is captured by deadlines to method calls. Every method activation in Real-Time ABS has an associated deadline, which decrements with the passage of time. This deadline can be accessed inside the method body with the expression deadline(). Deadlines are soft; i.e., deadline() may become negative but this does not in itself block the execution of the method. By default the deadline associated with a method activation is infinite, so in an untimed model deadlines will never be missed. Other deadlines may be introduced by means of call-site annotations. Real-Time ABS introduces two new data types into the functional sublanguage of ABS: Time, which has the constructor Time(r), and Duration, which has the constructors InfDuration and Duration(r), where r is a value of the type Rat of rational numbers. The accessor functions timeVal and durationValue return r for time and duration values Time(r) and Duration(r), respectively. Let o be an object which implements a method m. Below, we define a method n which calls m on o and specifies a deadline for this call, given as an annotation and expressed in terms of its own deadline. Remark that if its own deadline is InfDuration, then the deadline to m will also be unlimited. The function scale(d,r) multiplies a duration d by a rational number r (the definition of scale is straightforward).\nInt n (T x){ [Deadline: scale(deadline(),0.9)] return o.m(x); } Explicit Time In the explicit time model of Real-Time ABS, the execution time of computations is modeled using duration statements duration(e1,e2) with best- and worst-case execution times e1 and e2. These statements are inserted into the model, and capture execution time which does not depend on the system’s deployment architecture. Let f be a function defined in the functional sublanguage of ABS, which recurses through some data structure x of type T, and let size(x) be a measure of the size of this data structure x. Consider a method m which takes as input such a value x and returns the result of applying f to x. Let us assume that the time needed for this computation depends on the size of x; e.g., the computation time is between a duration 0.5*size(x) and a duration 4*size(x). An interface I which provides the method m and a class C which implements I, including the execution time for m using the explicit time model, are specified as follows:\ninterface I { Int m(T x) } class C implements I { Int m (T x){ duration(0.5*size(x), 4*size(x)); return f(x); } } Implicit Time In the implicit time model of Real-Time ABS, the execution time is not specified explicitly in terms of durations, but rather observed on the executing model. This is done by comparing clock values from a global clock, which can be read by an expression now() of type Time. We specify an interface J with a method p which, given a value of type T, returns a value of type Duration, and implement p in a class D such that p measures the time needed to call the method m above, as follows:\ninterface J { Duration p (T x) } class D implements J (I o) { Duration p (T x){ Time start; Int y; start = now(); y=o.m(x); return timeDifference(now(),start); } } Observe that by using the implicit time model, no assumptions about execution times are specified in the model above. The execution time depends on how quickly the method call is effectuated by the called object. The execution time is simply measured during execution by comparing the time before and after making the call. As a consequence, the time needed to execute a statement with the implicit time model depends on the capacity of the chosen deployment architecture and on synchronization with (slower) objects.\nModeling Deployment Architectures in ABS Deployment Components A deployment component in Real-Time ABS captures the execution capacity associated with a number of concurrent object groups. Deployment components are first-class citizens in Real-Time ABS, and provide a given amount of resources which are shared by their allocated objects. Deployment components may be dynamically created depending on the control flow of the ABS model or statically created in the main block of the model. We assume a deployment component environment with unlimited resources, to which the root object of a model is allocated. When objects are created, they are by default allocated to the same deployment component as their creator, but they may also be allocated to a different component. Thus, a model without explicit deployment components runs in environment, which does not impose any restrictions on the execution capacity of the model. A model may be extended with other deployment components with different processing capacities. Given the interfaces I and J and classes C and D defined in above, we can for example specify a deployment architecture in which two C objects are deployed on different deployment components server1 and server2, and interact with the D objects deployed on a deployment component clientServer. Deployment components in Real-Time ABS have the type DC and are instances of the class DeploymentComponent. This class takes as parameters a name, given as a string, and a set of restrictions on resources. The name is mainly used for monitoring purposes. Here we focus on resources reflecting the components’ processing capacity, which are specified by the constructor CPUCapacity(r), where r represents the amount of abstract processing resources available between observable points in time. Below, we create three deployment components Server1, Server2, and ClientServer, with the processing capacities 6, 3, and unlimited (i.e., ClientServer has no resource restrictions). The local variables server1, server2, and clientServer refer to these three deployment components, respectively. Objects are explicitly allocated to the servers by annotations; below, object1 is allocated to Server1, etc.\n{ // This main block initializes a static deployment architecture: DC server1 = new DeploymentComponent(\"Server1\",set[CPUCapacity(6)]); DC server2 = new DeploymentComponent(\"Server2\",set[CPUCapacity(3)]); DC clientServer = new DeploymentComponent(\"ClientServer\", EmptySet); [DC: server1] I object1 = new cog C; [DC: server2] I object2 = new cog C; [DC: clientServer] J client1monitor = new cog D(object1); [DC: clientServer] J client2monitor = new cog D(object2); } The figure depicts this deployment architecture and the artefacts introduced into the modeling language. Since all objects are allocated to a deployment component (which is environment unless overridden by an annotation), we let the expression thisDC() evaluate to the deployment component of an object. For convenience, a call to the method total(\"CPU\") of a deployment component returns its total amount of allocated CPU resources.\nResource Costs The available resource capacity of a deployment component determines how much computation may occur in the objects allocated to that component. Objects allocated to the component compete for the shared resources in order to execute, and they may execute until the component runs out of resources or they are otherwise blocked. For the case of CPU resources, the resources of the component define its processing capacity between observable (discrete) points in time, after which the resources are renewed.\nCost models The cost of executing statements in the ABS model is determined by a default value which is set as a compiler option (e.g., defaultcost=10). However, the default cost does not discriminate between statements and we may want to introduce a more refined cost model. For example, if e is a complex expression, then the statement x=e should have a significantly higher cost than skip in a realistic model. For this reason, more fine-grained costs can be inserted into Real-Time ABS models by means of annotations. For example, let us assume that the cost of computing the function f(x) defined in the section on Real-Time ABS may be given as a function g which depends on the size of the input value x. In the context of deployment components, we may redefine the implementation of interface I above to be resource-sensitive instead of having a predefined duration as in the explicit time model. The resulting class C2 can be defined as follows:\nclass C2 implements I { Int m (T x){ [Cost: g(size(x))] return f(x); } } It is the responsibility of the modeler to specify an appropriate cost model. A behavioral model with default costs may be gradually refined to provide more realistic resource-sensitive behavior. For the computation of the cost functions such as g in our example above, the modeler may be assisted by the COSTABS tool, which computes a worst-case approximation of the cost for f in terms of the input value x based on static analysis techniques, when given the ABS definition of the expression f. However, the modeler may also want to capture resource consumption at a more abstract level during the early stages of system design, for example to make resource limitations explicit before a further refinement of a behavioral model. Therefore, cost annotations may be used by the modeler to abstractly represent the cost of some computation which remains to be fully specified. For example, the class C3 below represents a draft version of our method m in which the worst-case cost of the computation is specified although the function f has yet to be introduced:\nclass C3 implements I { Int m (T x){ [Cost: size(x)*size(x)] return 0; } }",
    "description": "An introduction to time and resource modeling in ABS.",
    "tags": [],
    "title": "Resource Modeling Tutorial",
    "uri": "/documentation/tutorials/resources/index.html"
  },
  {
    "breadcrumb": "The ABS Language",
    "content": "The ABS language reference is the authoritative guide to what constitutes a legal ABS model, how to specify a Software Product Line, and how to use annotations to model time and resources.\nThere are some examples that walk through a small but complete ABS model to illustrate various modeling techniques.\nWe offer tutorials for the ABS language itself, as well as most tools that use ABS as an input language.",
    "description": "The ABS language reference is the authoritative guide to what constitutes a legal ABS model, how to specify a Software Product Line, and how to use annotations to model time and resources.\nThere are some examples that walk through a small but complete ABS model to illustrate various modeling techniques.\nWe offer tutorials for the ABS language itself, as well as most tools that use ABS as an input language.",
    "tags": [],
    "title": "Documentation",
    "uri": "/documentation/index.html"
  },
  {
    "breadcrumb": "The ABS Language \u003e Getting Started",
    "content": "We provide support for Emacs, Atom and Visual Studio Code.\nEmacs The abs-mode package provides support for ABS in the Emacs editor.\nInstallation instructions are at https://github.com/abstools/abs-mode.\nAtom The Atom editor support can be found at https://github.com/abstools/language-abs. ABS support for Atom currently cannot be installed from the offical Package repository and has to be installed manually; see https://github.com/abstools/language-abs for instructions.\nVisual Studio Code ABS editing support for Visual Studio Code can be installed as a .vsix file from the latest release, see https://github.com/abstools/abs-vs-code for detailed instructions.",
    "description": "We provide support for Emacs, Atom and Visual Studio Code.",
    "tags": [],
    "title": "Installing Editor Support",
    "uri": "/getting_started/editor-support/index.html"
  },
  {
    "breadcrumb": "The ABS Language \u003e Documentation \u003e Tutorials",
    "content": "CostABS is a a static analyzer for automatically inferring upper/lower bounds on the worst/best-case Resource usage (a.k.a. cost) of ABS programs. The inferred upper bounds have important applications in the fields of program optimization, verification and certification. CostABS is parametric on the cost model, i.e., the type of cost that the user wants to infer (e.g., number of steps, amount of memory allocated, amount of data transmitted, etc.), and it supports different notions of cost such as sequential, parallel, peak, etc.\nIn this tutorial, we overview the different features of CostABS by example. All examples are linked to the collaboratory where you can directly replay the steps described in the tutorial.\nResource Analysis with SACO In what follows we present how to use EasyInterface with the different analyses that CostABS is able to perform with some examples.\nWe first show how to start to use CostABS within the ABS collaboratory. For this, we must first select the analysis in the top pull-down menu, and, for executing the analysis, we click on Run. The Clear button (top right) removes all previous results.\nThe parameters of the selected analysis can be configured by clicking on the Settings button located in the top-left corner of the EasyInterface page. The results of the selected analysis are presented in the console at the bottom of the screen. This can be done by means of graphs, text messages, markers, highlighters in the code, and interactions among them. In the following, we describe the use of CostABS by analyzing several examples.\nBasic Resource Analysis Let us start by performing the basic resource analysis computed by CostABS and described in the paper “SACO: Static Analyzer for Concurrent Objects”. To do it, open the file VendingMachine_init.abs , which contains the following code:\nmodule VendingMachine_init; interface VendingMachine { Unit insertCoin(); Unit insertCoins( Int nCoins ); Int retrieveCoins(); } interface PrettyPrinter { Unit showIncome( Int nCoins ); Unit showCoin(); } class IVendingMachine( Int coins, PrettyPrinter out ) implements VendingMachine{ Unit insertCoin(){ coins = coins + 1; } Unit insertCoins( Int nCoins ){ while( nCoins \u003e 0 ){ nCoins = nCoins - 1; Fut\u003cUnit\u003e f = this ! insertCoin(); await f?; } } [coins \u003c max(coins)] Int retrieveCoins(){ Int total = 0; while( coins \u003e 0 ){ coins = coins - 1; Fut\u003cUnit\u003e f = out ! showCoin(); //await f?; total = total + 1; } return total; } } class IPrettyPrinter implements PrettyPrinter{ Unit showIncome( Int nCoins ){ /*Show something*/ } Unit showCoin(){ /*Show something*/ } } class IMain { Unit main( Int n ){ PrettyPrinter o = new IPrettyPrinter(); VendingMachine v = new IVendingMachine( 0, o ); v ! insertCoins(n); Fut\u003cInt\u003e f = v ! retrieveCoins(); await f?; Int total = f.get; o ! showIncome( total ); } } By selecting Resource Analysis and clicking on Settings a pop-up window appears and shows the configuration that allows us to set up the parameters for the analysis. The following parameters are available:\nCost model The cost model indicates the type of resource that we are interested in measuring. The user can select among the following cost metrics: termination (only termination is proved), steps (counts the number of executed instructions), objects (counts the number of executed new instructions), tasks (counts the number of asynchronous calls to methods), memory (measures the size of the created data structures), data transmitted (measures the amount of data transmitted among the distributed objects), user-defined model (allows to write annotations in the code of the form [cost == expr] and the analysis accumulates the cost specified by the user in expr every time this program point is visited). Cost centers This option allows us to decide whether we want to obtain the cost per cost center (i.e., for each of the abstract objects inferred by the analysis) or a monolithic expression that accumulates the whole computation in the distributed system. The value no refers to the latter case. If we want to separate the cost per cost center, we have again two possibilities. The option class shows the cost of all objects of the same class together, while objectindicates the cost attributed to each abstract object. Asymptotic bounds Upper bounds can be displayed in asymptotic or non-asymptotic form. The former one is obtained by removing all constants and subsumed expressions from the non-asymptotic cost, only showing the complexity order. Symbolic or numeric Next, if the cost model is memory or objects, the upper bounds can be shown either symbolically, in terms of symbolic sizes (we use size(A) to refer to the size of an object of type A), or numeric, by assigning a predefined measure to them. Debug sets the verbosity of the output (the higher the number, the more verbose the output). Rely Guarantee performs the resource analysis taking into account the possible interleavings in the tasks execution (as described in the paper “Termination and Cost Analysis of Loops with Concurrent Interleavings”). Peak Cost Analysis computes the peak cost analysis for all objects which are identified (see the paper ”Peak Cost Analysis of Distributed Systems”). Parallel Cost Analysis computes the parallel cost analysis of the program (see the paper “Parallel Cost Analysis of Distributed Systems”). Non-cumulative Cost Analysis computes the non-cumulative cost of the program (see the paper “Non-cumulative Resource Analysis”). Backend of the Analysis SACO uses PUBS or CoFloCo as backend to solve the cost equations (see the technical report “Resource Analysis of Complex Programs with Cost Equations”). Conditional Upper Bounds computes a set of conditional upper bounds (UBs) according to some conditions on the input parameters (see the technical report “Resource Analysis of Complex Programs with Cost Equations”). Timed Cost Analysis computes the cost analysis in time (see this technical report). Let us analyze the program VendingMachine_init.abs with the default values, except for the Asymptotic bounds parameter that must be set to yes. Click on Refresh Outline and select the entry method (method main of class IMain) in the Outline (the region on the right of the page). Then click on Run to perform the analysis. The result should be shown in the console as follows:\nMethod IMain.main terminates?: YES UB for 'IMain.main'(this,n,max(coins)) = nat(n)+nat(max(coins)) It can be seen in the resource analysis results given by CostABS that the upper bound is linear and it is a function on n (the input parameter of main) and on the maximum value that the field coins can take, denoted max(coins). Variable n is wrapped by function nat previously defined to avoid negative costs. The upper bound is shown in the console view and also at the method’s header when the mouse passes over the marker in line 48 in the program.\nNow, let us analyze the main method of the file VendingMachine.abs , which contains the following code:\nmodule VendingMachine; interface VendingMachine { Unit insertCoin(); Unit insertCoins( Int nCoins ); Int retrieveCoins(); } interface PrettyPrinter { Unit showIncome( Int nCoins ); Unit showCoin(); } interface Main{ Unit main( Int n ); } class IVendingMachine( Int coins, PrettyPrinter out ) implements VendingMachine{ Unit insertCoin(){ coins = coins + 1; } Unit insertCoins( Int nCoins ){ while( nCoins \u003e 0 ){ nCoins = nCoins - 1; Fut\u003cUnit\u003e f = this ! insertCoin(); await f?; } } Int retrieveCoins(){ Int result = 0; while( coins \u003e 0 ){ coins = coins - 1; Fut\u003cUnit\u003e f = out ! showCoin(); await f?; result = result + 1; } return result; } } class IPrettyPrinter implements PrettyPrinter{ Unit showIncome( Int nCoins ){ /*Show something*/ } Unit showCoin(){ /*Show something*/ } } class IMain implements Main{ Unit main( Int n ){ PrettyPrinter o = new IPrettyPrinter(); VendingMachine v = new IVendingMachine( 0, o ); v ! insertCoins(n); Fut\u003cInt\u003e f = v ! retrieveCoins(); await f?; Int result = f.get; o ! showIncome( result ); } } This file is just like the previous example, but includes the await instruction at line 37 that was commented out in the previous program. Analyze this program with the same configuration as before: default setting values, except for the asymptotic bounds parameter set to yes. Click on Refresh Outline and select the entry method (method main of class IMain) in the outline. Then click on Run to perform the analysis. The results will be shown like this:\nMethod IMain.main terminates?: UNKOWN UB for 'IMain.main'(this,n) = nat(n)+c(failed(no_rf,[scc=7,cr=entrywhile_1/4])) The analyzer shows, by using a warning marker (see line 41), that the resource analysis cannot infer an upper bound nor guarantee the termination of the program.\nRely-Guarantee Resource Analysis Info NOTE: this analysis is not currently available.\nLet us now perform the rely-guarantee resource analysis, described in the paper ”Termination and Cost Analysis of Loops with Concurrent Interleavings“, on the main method of the VendingMachine.abs file. To do so, we set the option Rely Guarantee to yes and the Cost Model to termination.\nAfter applying the analysis, it can be seen on the default console that CostABS proves that all methods of the program terminate. Let us now slightly modify the example to make method insertCoins non-terminating by removing line 35 with the instruction coins = coins – 1. The analysis information is displayed as follows. For each strongly connected component(SCC) (SCC-while loops and recursive methods are basically the SCCs in a program), the analysis places a marker in the entry line to the SCC. If the SCC is terminating (eg. line 25), by clicking on the marker, the lines that compose this SCC are highlighted in yellow. On the other hand, if the SCC is non-terminating (line 34), by clicking on the marker, CostABS highlights the lines of the SCC in blue. Besides the markers, the list of all SCCs of the program and their computed termination results are printed by CostABS on the console.\nAt this point, let us perform the rely guarantee resource analysis to infer the cost of the program. Restore the original code of line 35, click on Settings and select the Steps cost model with the option Rely guarantee set to yes. Then click on Run to perform the analysis.\nThe resulting upper bound obtained is a function in terms on n (the input parameter of main) and in terms of the maximum value that field coins can take, denoted max(coins). We can observe that the cost of main is linear with respect to both. In addition, CostABS shows a marker to the left of each method header to display their corresponding upper bounds.\nLoad Balance At this point, let us use the resource analysis to study the load balance of the program Performance.abs , which contains the following code:\nmodule Parallel; import * from ABS.StdLib; interface I { Unit m (Int n); Unit p (Int n, I x); Unit m2 (Int n); Unit q (); } class C implements I{ Unit m (Int n) { I a = new C(); while (n \u003e 0) { a!p(n, a); n = n - 1; } } Unit mthis (Int n) { I a = new C(); while (n \u003e 0) { a!p(n, this); n = n - 1; } } Unit p (Int n, I x) { while (n \u003e 0) { x!q(); n = n - 1; } } Unit m2 (Int n) { while (n \u003e 0) { I a = new C (); a!p(n, a); n = n - 1; } } Unit q () { skip; } } As the concurrency unit of ABS is the object, this analysis uses the cost centers to assign the cost of each execution step to the object where the step is performed. We start by applying the Resource Analysis and setting the option Cost Centers to object in the settings. Then click on Refresh Outline and select the method C.m on the right region of the page. Finally, click on Run to perform the analysis. In the console, we see the following output:\nUB Object Sensitive for C.m(this,n): 6*c([C.m])+nat(n)* (2*c([C.m])+5*c([C.m])+3*c([1,C.m])+nat(n)* (2*c([1,C.m])+5*c([1,C.m])+2*c([1,C.m]))+2*c([1,C.m])+c([1,C.m]))+2*c([C.m])+c([C.m])+c([1,C.m]) UB for cobox ([13,12],C): 1+nat(n)* (6+9*nat(n)) UB for cobox ([12],C.m): 9+7*nat(n) CostABS returns the cost centers in the program, one cost center labelled with [12] which corresponds to the object that executes C.m and another one labelled with [13,12], which abstracts the object created at line 13. The labels of the nodes contain the program lines where the corresponding object is created. That is, the node labeled as [13,12] corresponds to the C object, created at line 13 while executing the main method, the node identified by line 12. In addition, CostABS shows a graph with both nodes in the Console Graph view at the bottom of the screen. By clicking on the node [12], CostABS shows a dialog box with the upper bound on the number of steps performed by this node. Similarly, by clicking on the node [13,12], it shows the number of steps that can be executed by the object identified with [13,12].\nWe can observe that the node [12] performs a number of steps that is bounded by a linear function on the input parameter n, while in the node [13,12] the number of steps is bounded by a quadratic function on n. If we analyze method C.mthis, the cost is distributed in a different way. In this case, both nodes [20] and [21,20] have a quadratic upper bound on the number of steps performed by each node. The difference between both methods is that the call x!q() at line 30 is performed in object [13,12] in the former case, and in object [20] in the latter.\nWe can obtain the number of instances of each object we can have in each node. Select C.m2 and unselect the previously selected methods on the outline on the right of the page, and perform the Resource Analysis, setting the options Cost Model to Objects and Cost Centers to Object. It can be seen in the output of CostABS that the number of instances of the object identified by [37,35] is bounded by n (the input argument of method m2). Finally, we can apply the resource analysis to C.m2 selecting Cost Model to Steps to obtain the results of the analysis for this method regarding the number of steps.\nTransmission Data Sizes Now, let us perform the transmission data size analysis to the following code:\nmodule DemoTraffic; import * from ABS.StdLib; interface II { Unit work (Int n, List\u003cInt\u003e l); } interface IS { Int process (List\u003cInt\u003e l); } class Master (IS s) implements II { Unit work (Int n, List\u003cInt\u003e l){ while (n\u003e0) { l = Cons(1,l); Fut\u003cInt\u003e q = s!process(l); q.get; n = n - 1; } } } class Slave () implements IS{ Int process (List\u003cInt\u003e l) {return 1;} } class IMain { Unit main (List\u003cInt\u003e l, Int n) { IS s = new Slave(); II m = new Master(s); m!work(n,l); } } Open the file DataTransmitted.abs . To analyze this file with the transmission data size analysis, select the analysis Resource Analysis (SACO) and set the option Cost Model to Traffic. Then refresh the outline and apply the analysis to the method IMain.main.\nWhen the analysis is applied, the console will show the upper bound expressions for all possible pairs of objects identified by the analysis:\nUB Object Sensitive for IMain.main(this,l,n): c(o([IMain.main],[2,IMain.main],Master.work))* (1+c(i)+nat(l))+c(o([2,IMain.main],[IMain.main],Master.work))* (1+c(i))+c(o([IMain.main],[2,IMain.main],Master.init))* (1+c(i))+c(o([2,IMain.main],[IMain.main],Master.init))*c(i)+c(o([IMain.main],[1,IMain.main],Slave.init))*c(i)+c(o([1,IMain.main],[IMain.main],Slave.init))*c(i)+nat(n)* (c(o([2,IMain.main],[1,IMain.main],Slave.process))* (c(i)+nat(l+2*n))+c(o([1,IMain.main],[2,IMain.main],Slave.process))* (1+c(i))) UB for interactions between ([31],[32,31]): c(i) UB for interactions between ([31],[33,31]): 2+nat(l)+2*c(i) UB for interactions between ([33,31],[32,31]): nat(n)* (c(i)+nat(l+2*n)) UB for interactions between ([32,31],[31]): c(i) UB for interactions between ([33,31],[31]): 1+2*c(i) UB for interactions between ([32,31],[33,31]): nat(n)* (1+c(i)) For example, the last line of the console output is the upper bound of the size of the data transmitted from the node [32,31] to the node [33,31], that are the Slave and Master objects created at line 32 and line 33, respectively. We can observe that this upper bound linearly depends on the input parameter n, which is the number of times the method process in the Slave object is invoked. On the other hand, the data transmitted from the Master object [33,31] to the Slave object [32,31] is different, as the invocation contains the list l which is passed as argument to the method process. In this case, the upper bound is a quadratic function on the parameter n, as the list passed as argument grows at each iteration of the loop at line 16, and this loop iterates n times.\nIn addition to the console information, the graph in output tab Console Graph shows the objects creation. By clicking on a node in the graph, a message outputs the UBs (upper bounds) for all transmissions data sizes that the selected object can perform and the objects involved in such transmissions. For example, by clicking on the node [32,31], which corresponds to the Master object, we can see the upper bounds on the data transmitted (incoming and outgoing transmissions) from this object. As before, the labels of the nodes contain the program lines where the corresponding object is created. For instance, the node labeled as [32,31] corresponds to the Master object, created at line 32 while executing the main method, the object identified by line 31. In such upper bounds, the cost expression c(i) represents the cost of establishing the communication.\nNon-Cumulative Cost We can illustrate the analysis for computing the non-cumulative cost with the file Noncumulative.abs , which contains the following code:\nmodule Noncumulative; import * from ABS.StdLib; class IMain { Unit main (Int s, Int n) { [x == acquire(10)] Int i= 0; [r == acquire(100)] i = 0; [r == acquire(s)] i = 1; [r == release()] i = 2; [y == acquire(n)] i = 3; [x == release()] i = 4; } } In Settings, restore the default values and set the option noncumulative_cost to yes. Then refresh the outline and select the method IMain.main. The results obtained after clicking Run show that we have two sets of program points that can lead to the maximum on the number of resources acquired, as well as their corresponding upper bound expressions. The set [L6,L8,L10] corresponds to the acquireinstructions at lines 6, 8 and 10 of the program. With this set of acquire instructions, we obtain an upper bound of the number of resources that linearly depends on the input parameter s because of the acquire at line 10. The set [L6,L8,L14] can also lead to the maximum number of resources acquired, if the actual value of the input parameter n is larger than s.\nPeak Cost Analysis Let us continue by performing the peak cost analysis to the program VendingMachine_init.abs . Similarly to other analyses, we first select the entry method (method main in class IMain) in the outline view and start the Resource Analysis (SACO) with default options, with the exception of the option Peak Cost, which must be set to yes. After clicking Run, the peak cost analysis outputs in the console.\nClosure time 2 ms. Direct mhp time 0 ms. Indirect mhp time 24 ms. Configurations found for queue [49,48] -- IPrettyPrinter.showIncome,IPrettyPrinter.showCoin -- IPrettyPrinter.init UBs for the configurations of queue [49,48] -- UB_k for [49,48]-[IPrettyPrinter.showIncome,IPrettyPrinter.showCoin]): 2+2*nat(max(coins)-1) -- UB_k for [49,48]-[IPrettyPrinter.init]): 0 Configurations found for queue [50,48] -- IVendingMachine.insertCoins,IVendingMachine.retrieveCoins,IVendingMachine.insertCoin -- IVendingMachine.init UBs for the configurations of queue [50,48] -- UB_k for [50,48]-[IVendingMachine.insertCoins,IVendingMachine.retrieveCoins,IVendingMachine.insertCoin]): 13+14*nat(n)+13*nat(max(coins)-1) -- UB_k for [50,48]-[IVendingMachine.init]): 0 For each identified ABS object, all possible queue configurations are shown. A queue configuration is the set of tasks that can be in the task queue simultaneously. For each queue configuration, the tasks involved in the configuration are shown. In addition, the total cost associated with the configuration is displayed as well.\nThe analysis of the program VendingMachine_init.abs shows that there are two possible queue configurations for each object identified in the program. For example, for the object [49,48] one of the configurations contains tasks for methods showIncome and showCoin, and the number of steps executed by those tasks linearly depends on the value of the field coins.\nAs before, the output tab Console Graph also shows a graph where the labels of the nodes contain the program lines where the corresponding object is created. For instance, the node labeled as [49,48] corresponds to the PrettyPrinter object, created at line 49 while executing the main method which starts at line 48. By clicking on a node, the queue configurations that have been identified and their costs are shown in a message.\nParallel Cost Let us perform the parallel cost analysis described in the paper “Parallel Cost Analysis of Distributed Systems”. To do so, we open the file Parallel.abs , which contains the following code:\nmodule Parallel; import * from ABS.StdLib; interface IX { Unit p (IY y); } interface IY { Unit q (); Unit s (); } class X implements IX { Unit p (IY y) { skip; y!s(); Int method_end = 0; } } class Y implements IY { Unit q () { Int method_end = 0; } Unit s () { Int method_end = 0; } } class IMain { Unit main () { IX x = new X (); IY y = new Y (); x!p(y); skip; y!q(); Int method_end = 0; } } Select the entry method IMain.main in the outline and apply the Resource Analysis by restoring the default values and setting the option Parallel Cost to yes. The analysis results show the computed upper bound expressions obtained for all paths identified in the DFG (distributed flow graph) of the program. In addition, the result shows the number of nodes and edges of the computed DFG.\nClosure time 1 ms. Direct mhp time 0 ms. Indirect mhp time 3 ms. DFG Number of Nodes: 11 DFG Number of Edges: 12 DFG Number of Exit nodes: 4 Number of Paths found: 16 The Parallel Cost for IMain.main(this) is the maximum of the expressions (4): UB Expression: 10 UB Expression: 14 UB Expression: 13 UB Expression: 9 Cost Analysis in Time Let us continue by performing the cost analysis in time to the program in Timed.abs , with the following code:\nmodule Timed; interface Job{ Unit start(Int dur); } class IMain{ Unit main(Int n){ while(n\u003e0){ Job job=new local Job(); job!start(10);\tawait duration(1,1); n= n-1; } } } class Job implements Job{ Unit start(Int dur){ while(dur\u003e0){ [Cost: 1] dur=dur-1; await duration(1,1); } } } Select the entry method IMain.main in the outline of the program. Then, select the Resource Analysis and set the option Timed Cost to yes. After applying the analysis, the output of SACO shows\nMethod IMain.main terminates?: YES UB for 'IMain.main'(this,n,time,target) = n*c(condition([[1*time=1,-1*n+1*_G13533=1,-1*target\u003e= -9,1*_G13533\u003e=2,-1*_G13533+1*target\u003e=0]])) Method IMain.main terminates?: YES UB for 'IMain.main'(this,n,time,target) = 0*c(condition([[1*time=1,-1*n+1*_G13533=1,1*_G13533\u003e=2,-1*_G13533+1*target\u003e=9],[1*time=1,1*_G13533=1,-1*n\u003e=0,1*target\u003e=1]])) Method IMain.main terminates?: YES UB for 'IMain.main'(this,n,time,target) = 1*c(condition([[1*time=1,1*target=1,-1*n+1*_G13542=1,1*_G13542\u003e=3],[1*time=1,-1*n+1*_G13542=1,-1*target+1*_G13542= -8,1*_G13542\u003e=2],[1*n=1,1*time=1,1*target=1,1*_G13542=2]])) Method IMain.main terminates?: YES UB for 'IMain.main'(this,n,time,target) = 9*c(condition([[1*time=1,-1*n+1*_G13533=1,1*target\u003e=11,-1*target+1*_G13533\u003e= -7,-1*_G13533+1*target\u003e=0],[1*time=1,1*target=10,-1*n+1*_G13533=1,-1*_G13533\u003e= -10,1*_G13533\u003e=3]])) Method IMain.main terminates?: YES UB for 'IMain.main'(this,n,time,target) = 10*c(condition([[1*time=1,-1*n+1*_G13533=1,1*target\u003e=11,-1*target+1*_G13533\u003e=2],[1*time=1,1*target=10,-1*n+1*_G13533=1,1*_G13533\u003e=12]])) Method IMain.main terminates?: YES UB for 'IMain.main'(this,n,time,target) = 11*c(condition([[1*time=1,-1*target+1*n=0,-1*_G13545+1*n= -1,1*n\u003e=11],[1*n=10,1*time=1,1*target=10,1*_G13545=11]])) Method IMain.main terminates?: YES UB for 'IMain.main'(this,n,time,target) = (n+1)*c(condition([[1*time=1,-1*n+1*_G13536=1,-1*target\u003e= -9,1*target\u003e=2,-1*target+1*_G13536\u003e=2],[1*time=1,-1*target+1*n=0,-1*_G13536+1*n= -1,-1*n\u003e= -9,1*n\u003e=2]])) CoFloCo Backend Finally, let us analyze the program CoFloCoExample.abs by using CoFloCo as backend. In this case, the file contains the following code:\nmodule Parallel; import * from ABS.StdLib; class C { Bool nondet=False; Unit m1 (Int i, Int dir, Int n) { while (0\u003ci \u0026\u0026 i \u003c n) { if (dir == 1) { i = i + 1; } else { i = i - 1; } } } Unit m2 (Int x, Int y, Int a, Int r) { while (x \u003e 0 \u0026\u0026 y \u003e 0) { if (nondet) { x = x - 1; y = r; } else { y = y - 1; } suspend; } } Unit m3 (Int x, Int y, Int a) { while (x \u003e 0) { while (y \u003e 0 \u0026\u0026 nondet) { y = y - 1; suspend; } x = x - 1; } } } We can select the method of interest, that is, C.m, C.m2 or C.m3 and then perform the resource analysis with the default options except the option Backend, which must be set to CoFloCo. After applying the analysis, SACO shows the results of the analysis of C.m with CoFloCo.",
    "description": "CostABS is a a static analyzer for automatically inferring upper/lower bounds on the worst/best-case Resource usage (a.k.a. cost) of ABS programs.  In this tutorial, we overview the different features of CostABS by example.",
    "tags": [],
    "title": "Resource Analysis with CostABS",
    "uri": "/documentation/tutorials/costabs/index.html"
  },
  {
    "breadcrumb": "The ABS Language \u003e Documentation",
    "content": "This page features a list of examples – small and large complete ABS models that illustrate various modeling techniques.\nThe Monty Hall ProblemModeling simple behavior, getting complex results.\nModeling and Visualizing Calendar TimeAn example for using Real-Time ABS to calculate with real (calendar) dates and times and visualize them on a graphical timeline.\nDisplaying geo-annotated informationAn example on how to display data from ABS on a map via the Model API\nModeling and Visualizing A Water Tank ControllerAn example for discrete-time simulation of a simple physical system and controller using Real-Time ABS.\nModeling ResourcesAn example on how to model distributed application deployments\nABS Model of a Multicore Memory SystemA model of the MSI cache coherency protocol.",
    "description": "This page features a list of examples – small and large complete ABS models that illustrate various modeling techniques.\nThe Monty Hall ProblemModeling simple behavior, getting complex results.\nModeling and Visualizing Calendar TimeAn example for using Real-Time ABS to calculate with real (calendar) dates and times and visualize them on a graphical timeline.\nDisplaying geo-annotated informationAn example on how to display data from ABS on a map via the Model API",
    "tags": [],
    "title": "Examples",
    "uri": "/documentation/examples/index.html"
  },
  {
    "breadcrumb": "The ABS Language",
    "content": "This page links ABS workshops, as well as selected research papers on the development and usage of the ABS modeling language and analysis tools.\nABS Workshops 2017 First International ABS Workshop: May 31–June 2, 2017, Oslo, Norway.\n2018 Second International ABS Workshop: May 28–May 30, 2018, Darmstadt, Germany. https://formbar.raillab.de/en/abs2018/\n2019 Third International ABS Workshop: May 13–May 15, 2019, Amsterdam, The Netherlands. https://www.cwi.nl/research/groups/formal-methods/events/third-international-workshop-on-the-abs-modeling-language-and-tools\n2021 Fourth International ABS Workshop: August 26–August 27, 2021, Virtual. https://formbar.raillab.de/en/abs-workshop-2021/\n2023 Fifth International ABS Workshop: October 04-06, 2023, Lyon, France. https://edkamb.github.io/ABS_23/\n2024 APM Workshop 2024: October 02-04, 2024, Turin, Italy. https://edkamb.github.io/APM_24/\nCase Studies G. Turin, A. Borgarelli, S. Donetti, E. B. Johnsen, S. L. Tapia Tarifa, and F. Damiani.\nA Formal Model of the Kubernetes Container Framework..\nLeveraging Applications of Formal Methods, Verification and Validation (ISoLA 2020). LNCS 12476. Springer, 2020.\nDOI: 10.1007/978-3-030-61362-4_32. Download a preprint.\nJ-C Lin, M-C Lee, I. C. Yu, and E. B. Johnsen.\nA configurable and executable model of Spark Streaming on Apache YARN.\nInternational Journal of Grid and Utility Computing. Volume 11(2). Indescience, 2020.\nDOI: 10.1504/IJGUC.2020.105531. Download a preprint.\nE. Kamburjan, R. Hähnle, and S. Schön Formal modeling and analysis of railway operations with active objects.\nScience of Computer Programming. Volume 166. Elsevier, 2018.\nDOI: 10.1016/j.scico.2018.07.001.\nE. Albert, F. de Boer, R. Hähnle, E. B. Johnsen, R. Schlatte, S. L. Tapia Tarifa, and P. Y. H. Wong.\nFormal modeling and analysis of resource management for cloud architectures: an industrial case study using Real-Time ABS.\nService Oriented Computing and Applications 8 (4):323-339, 2014.\nDOI: 10.1007/s11761-013-0148-0. Download a preprint.\nLanguage Development L. Tveito, E. B. Johnsen, and R. Schlatte.\nGlobal Reproducibility through Local Control for Distributed Active Objects.\nIn Proc. 23th International Conference on Fundamental Approaches to Software Engineering (FASE 2020), LNCS 12076. Springer , 2020.\nDOI: 10.1007/978-3-030-45234-6_7. Download a preprint.\nR. Schlatte, E. B. Johnsen, J. Mauro, S. L. Tapia Tarifa, and I. C. Yu .\nRelease the Beasts: When Formal Methods Meet Real World Data.\nFestschrift Farhad Arbab, LNCS 10865. Springer , 2018.\nDOI: 10.1007/978-3-642-25271-6_8. Download a preprint.\nE. Kamburjan.\nFrom post-conditions to post-region invariants: deductive verification of hybrid objects..\nIn 24th ACM International Conference on Hybrid Systems: Computation and Control (HSCC 2021). ACM , 2021.\nDOI: 10.1145/3447928.3456633.\nE. B. Johnsen, R. Hähnle, J. Schäfer, R. Schlatte, and M. Steffen.\nABS: A Core Language for Abstract Behavioral Specification.\nIn Proc. 9th Intl. Symp. on Formal Methods for Components and Objects (FMCO 2010), LNCS 6957. Springer , 2011.\nDOI: 10.1007/978-3-642-25271-6_8. Download a preprint.\nE. B. Johnsen, R. Schlatte, and S. L. Tapia Tarifa.\nIntegrating Deployment Architecture and Resource Consumption in Timed Object-Oriented Models.\nJournal of Logical and Algebraic Methods in Programming 84(1): 67-91, 2015.\nDOI: 10.1016/j.jlamp.2014.07.001. Download a preprint.\nJoakim Bjørk, Frank S. de Boer, Einar Broch Johnsen, Rudolf Schlatte, and S. L. Tapia Tarifa.\nUser-defined schedulers for real-time concurrent objects.\nInnovations Syst Softw Eng 9(1): 29-43 (2013).\nDOI: 10.1007/s11334-012-0184-5. Download a preprint.\nF. Damiani, R. Hähnle, E. Kamburjan, M. Lienhardt.\nA Unified and Formal Programming Model for Deltas and Traits.\nProc. 20th International Conference on Fundamental Approaches to Software Engineering (FASE 2017), LNCS 10202. Springer, 2017.\nDOI: 10.1007/978-3-662-54494-5_25. Download a postprint.\nSoftware Product Lines F. Damiani, R. Hähnle, E. Kamburjan, M. Lienhardt, L. Paolini.\nVariability modules for Java-like languages.\nProc. 25th ACM International Systems and Software Product Line Conference (SPLC 2021). ACM, 2021.\nDOI: 10.1145/3461001.3471143.\nF. Damiani, M. Lienhardt, R. Muschevici, I. Schaefer.\nAn Extension of the ABS Toolchain with a Mechanism for Type Checking SPLs.\nProc. 13th International Conference on Integrated Formal Methods (IFM 2017), LNCS 10510. Springer, 2017.\nDOI: 10.1007/978-3-319-66845-1_8. Download a postprint.\nDeductive Verification E. Kamburjan, C. C. Din, R. Hähnle and E. B. Johnsen.\nBehavioral Contracts for Cooperative Scheduling.\nIn Deductive Software Verification: Future Perspectives, LNCS 12345. Springer, 2020.\nDOI: 10.1007/978-3-030-64354-6_4. Download a preprint.\nC. C. Din, R. Bubel and R. Hähnle.\nKeY-ABS: A Deductive Verification Tool for the Concurrent Modelling Language ABS.\nIn Proc. 25th Intl. Conf. on Automated Deduction (CADE 2015), LNCS 9195. Springer, 2015.\nDOI:10.1007/978-3-319-21401-6_35. Download a preprint.\nC. C. Din, S. L. Tapia Tarifa, R. Hähnle and E. B. Johnsen.\nHistory-Based Specification and Verification of Scalable Concurrent and Distributed Systems.\nIn Proc. 17th Intl. Conf. on Formal Engineering Method (ICFEM 2015), LNCS 9407. Springer, 2015.\nDOI: 10.1007/978-3-319-25423-4_14. Download a preprint.\nAnalysis C. Laneve, M. Lienhardt, K. I Pun, and G. Román-Díez.\nTime analysis of actor programs.\nJournal of Logical and Algebraic Methods in Programming, Volume 105, Elsevier, 2019.\nDOI: 10.1016/j.jlamp.2019.02.007.\nA. Garcia, C. Laneve, and M. Lienhardt.\nStatic analysis of cloud elasticity.\nScience of Computer Programming, Volume 147, Elsevier, 2017.\nDOI: 10.1016/j.scico.2017.03.008.\nE. Albert, P. Arenas, A. Flores-Montoya, S. Genaim, M. Gómez-Zamalloa, E. Martin-Martin, G. Puebla, and G. Román-Díez.\nSACO: Static Analyzer for Concurrent Objects.\nIn Proc. 20th Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS 8413, Springer, 2014.\nDOI: 10.1007/978-3-642-54862-8_46. Download a preprint.\nE. Giachino, C. Laneve, and M. Lienhardt.\nA Framework for Deadlock Detection in ABS.\nJournal of Software and Systems Modeling, Volume 15(4), Springer, 2015.\nDOI: 10.1007/s10270-014-0444-y.\nABS Tools Rudolf Schlatte, Einar Broch Johnsen, Eduard Kamburjan and S. Lizeth Tapia Tarifa\nThe ABS simulator toolchain Science of Computer Programming. Volume 233. Elsevier, 2022.\nDOI: 10.1016/j.scico.2022.102861. Code Generation from ABS B. Nobakht and F. S. de Boer.\nProgramming with Actors in Java 8.\nIn Proc. of the 6th Intl. Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA’14). LNCS 8803. Springer, 2014.\nDOI: 10.1007/978-3-662-45231-8_4. Download a preprint. Model-based Deployment and Monitoring R. Hähnle and E. B. Johnsen.\nDesigning Resource-Aware Cloud Applications.\nIEEE Computer 48 (6), 2015.\nDOI: 10.1109/MC.2015.172. Download a preprint.\nB. Nobakht, S. de Gouw and F.S. de Boer.\nFormal Verification of Service Level Agreements Through Distributed Monitoring.\nIn Proc. 4th European Conf. on Service Oriented and Cloud Computing (ESOCC 2015). LNCS 9306, Springer, 2015.\nDOI: 10.1007/978-3-319-24072-5_9. Download a preprint.",
    "description": "This page links ABS workshops, as well as selected research papers on the development and usage of the ABS modeling language and analysis tools.\nABS Workshops 2017 First International ABS Workshop: May 31–June 2, 2017, Oslo, Norway.\n2018 Second International ABS Workshop: May 28–May 30, 2018, Darmstadt, Germany. https://formbar.raillab.de/en/abs2018/\n2019 Third International ABS Workshop: May 13–May 15, 2019, Amsterdam, The Netherlands. https://www.cwi.nl/research/groups/formal-methods/events/third-international-workshop-on-the-abs-modeling-language-and-tools\n2021 Fourth International ABS Workshop: August 26–August 27, 2021, Virtual. https://formbar.raillab.de/en/abs-workshop-2021/",
    "tags": [],
    "title": "Publications and Workshops",
    "uri": "/publications/index.html"
  },
  {
    "breadcrumb": "The ABS Language \u003e Documentation \u003e Tutorials",
    "content": "May-Happen-in-Parallel Analysis (MHP) ABS is a distributed language where different methods can be invoked asynchronously. Therefore, there can be several tasks executing their code at the same time. This simultaneity complicates the analysis and understanding of ABS programs, since (in general) there is a high level of parallelism. The MHP analysis alleviates this situation by computing, for each instruction, which other instructions could execute in parallel. This information can be very interesting for developers and testers, but it is crucial for the precision of many of the SACO analyses presented in the CostABS tutorial.\nThe result of the MHP analysis, described in the paper “Analysis of May-Happen-in-Parallel in Concurrent Objects”, is a set of pairs of instructions that could execute in parallel in any execution of the program. It is important to stress that this analysis computes an overapproximation of the parallelism. In other words, if a pair of instruction can execute in parallel, then they will be detected by the analysis; however, the analysis can incorrectly detect pairs of instructions that never execute in parallel when executing the program.\nMHP Analysis in the Collaboratory In order to apply the MHP Analysis in the Collaboratory, just:\nOpen the ABS program to analyze. Select MHP Analysis in the list of analyses. Refresh the list of methods in the right side (button Refresh Outline) and select the entry point of the analysis. Only one method or function can be selected as entry point. If none is selected then the main block will be considered the entry point. Press the Run button. Let us see the results of the MHP analysis in the VendingMachine.abs program selecting the main method from class IMain as the entry point. The analysis reports its results in two places. First, all the pairs of instructions that can be executed in parallel are printed in the console. This information is very detailed and verbose, but difficult to understand:\n... L28 (Await)[IVendingMachine.insertCoins(-[2,'IMain.main']-)] || L37 (Await)[IVendingMachine.retrieveCoins(-[2,'IMain.main']-)] L20 (Entry)[IVendingMachine.insertCoin(-[2,'IMain.main']-)] || L60 (Exit)[IMain.main(-['IMain.main']-)] ... The previous fragment shows that the instruction at L28 (the await instruction in method insertCoins) can happen in parallel with the instruction at L37 (the await instruction in method retrieveCoins), and the same for instructions at L20 and L60. However, the most comfortable way of inspecting the results of the MHP analysis is by navigating the code. Every considered instruction will have a blue arrow in its left margin. When clicking the arrow of an instruction, all the other considered instructions that can happen in parallel with it will be highlighted in yellow. For example, clicking on the arrow in L37 will show the instructions that can happen in parallel with it, which as expected include L28. We have mentioned “considered instruction” because, by default, the MHP analysis only takes into account those instructions that are entry/exit points of methods and await or release instructions. In order to obtain the full list of instructions that may happen in parallel, open the settings window (button Settings, option MHP analysis) and change the option Amount of considered points from Reduced to Full. With these new settings the analysis obtains the MHP information for all the instructions in the program.\nSince the MHP analysis is a sound overapproximation, instructions that cannot execute in parallel are never detected. For example, due to the await instruction at L57, the task retrieveCoins must be finished before continuing. Therefore, the await instruction at L37, which is inside retrieveCoins, cannot happen in parallel with the instructions after the await (L58 and L59) or the method showIncome that is invoked at L59. If we execute a full MHP analysis and select the arrow at L37, those fragments will not be highlighted.\nMHP Settings In addition to the Amount of considered points to compute all the pairs of instructions that can execute in parallel or only a the most important, the MHP analysis supports other important settings, as shown in the next figure:\nUsing these parameters we can adapt the behavior of the analysis:\nDebug information (0, 1, or 2): level of information that is printed in the console, where 0 is the lowest level. Points-to analysis precision (1, 2, 3 and 4): the precision that will be used in the point-to analysis that approximates the different objects that are created during execution. Condition synchronization MHP extension (no, yes): by default, the MHP analysis only considers simple await instructions involving one future variable (await f?;). When enabling this option, the analysis tries to use the information from await instructions that involve complex conditions like await this.x != null. Inter-Procedural Synchronization (no, yes): enables a refinement of the MHP analysis that obtains finer information about the finished task, thus producing more precise results in programs with inter-procedural synchronization.\nMay-Happen-in-Parallel with Inter-Procedural Synchronization Let us analyze with SACO the program InterProcedural.abs with the Inter-Procedural Synchronization of the MHP analysis (described in the paper May-Happen-in-Parallel Analysis for Asynchronous Programs with Inter-Procedural Synchronization), as mentioned before.\nmodule Parallel; import * from ABS.StdLib; interface IO1 { Unit f (); } interface IO2 { Unit g (Fut\u003cUnit\u003e w); } class O1 implements IO1 { Unit f () { skip; } } class O2 implements IO2 { Unit g (Fut\u003cUnit\u003e w) { skip; await w?; skip; } } { Fut\u003cUnit\u003e x; Fut\u003cUnit\u003e y; IO1 o1 = new local O1(); IO2 o2 = new local O2(); x = o1!f(); y = o2!g(x); await y?; } If we apply the MHP analysis without inter-procedural synchronization, we obtain that L14 can happen in parallel with L34 because the analysis is not able to infer that when method g finishes its execution, method f has finished too (caused by the await instruction in L21).\nTo refine the MHP analysis, we set the option Inter-Procedural Synchronization to yes. Using this refinement we obtain that the only program points that can happen in parallel with L34 are the end of methods f and g, which means that both methods must have finished when L34 is reached.",
    "description": "The maypar static analysis tool finds pairs of program statements that possibly execute in parallel.",
    "tags": [],
    "title": "May-Happen-in-Parallel Analysis",
    "uri": "/documentation/tutorials/mhp/index.html"
  },
  {
    "breadcrumb": "The ABS Language \u003e Documentation",
    "content": "This page features a list of tutorials for most tools that work with the ABS language.\nConverted Tutorials Conversion from old tutorials is on-going and help is most welcome.\nLanguage TutorialThis tutorial gives an overview of the ABS language.\nResource Modeling TutorialAn introduction to time and resource modeling in ABS.\nResource Analysis with CostABSCostABS is a a static analyzer for automatically inferring upper/lower bounds on the worst/best-case Resource usage (a.k.a. cost) of ABS programs. In this tutorial, we overview the different features of CostABS by example.\nMay-Happen-in-Parallel AnalysisThe maypar static analysis tool finds pairs of program statements that possibly execute in parallel.\nResource Analysis with SRAWe prototype a static analysis technique that computes upper bounds of virtual machine usages in a dialect of ABS called vml.\nEnvisage / HATS Tutorials These tutorials were written during the Envisage and HaTS projects. The pdfs are provided as-is and might contain outdated information.\nInstallation Tutorial\nEasyInterface Tutorial\nResource Tutorial\nResource Analysis (SACO) Tutorial\nResource Analysis (SRA) Tutorial\nDeadlock Analysis (SACO) Tutorial\nDeadlock Analysis (SRA) Tutorial\nSystematic Testing (SYCO) \u0026 Test Case Generation (aPET) Tutorial\nSmart Deployer Tutorial\nKeY-ABS Tutorial\nModelling Auto-scalable Services Tutorial",
    "description": "This page features a list of tutorials for most tools that work with the ABS language.\nConverted Tutorials Conversion from old tutorials is on-going and help is most welcome.\nLanguage TutorialThis tutorial gives an overview of the ABS language.\nResource Modeling TutorialAn introduction to time and resource modeling in ABS.\nResource Analysis with CostABSCostABS is a a static analyzer for automatically inferring upper/lower bounds on the worst/best-case Resource usage (a.k.a. cost) of ABS programs. In this tutorial, we overview the different features of CostABS by example.",
    "tags": [],
    "title": "Tutorials",
    "uri": "/documentation/tutorials/index.html"
  },
  {
    "breadcrumb": "The ABS Language \u003e Documentation \u003e Examples",
    "content": "ABS provides a logical clock, a rational-valued global counter starting at 0 – see the Timed ABS chapter of the manual for details. This example shows how to use ABS to run simulations modeling real (calendar) time and visualize the resulting data in a timeline.\nThe code can be found at https://github.com/abstools/absexamples/tree/master/collaboratory/examples/time-and-date/\nModeling Time in ABS The following short ABS model creates a list of values together with the time when the value was produced. The results are stored in a Calendar object that is accessible via the ABS Model API.\nDuring the simulation, the method addValue is called with random values. The calendar object keeps track of the value and the time when it was added.\nThe calendar also makes two methods callable via the Model API: getValues returns a list of pairs of recorded time and value. The method getStartDate returns a string containing a date in ISO 8601 notation; this is the “real” start date that will be used in the simulation. The time values in the list returned by getValues will be interpreted as offset from that point in time.\nmodule CalendarTime; def String start_date() = \"2020-04-01\"; interface Calendar { [HTTPCallable] String getStartDate(); [HTTPCallable] List\u003cPair\u003cRat, Int\u003e\u003e getValues(); Unit addValue(Int value); } class Calendar implements Calendar { List\u003cPair\u003cRat, Int\u003e\u003e values = list[]; String getStartDate() { return start_date(); } List\u003cPair\u003cRat, Int\u003e\u003e getValues() { return reverse(values); } Unit addValue(Int value) { values = Cons(Pair(timeValue(now()), value), values); } } { [HTTPName: \"Calendar\"] Calendar c = new Calendar(); Int nRounds = 16; while (nRounds \u003e 0) { c!addValue(random(50)); await duration(1/4, 1/4); nRounds = nRounds - 1; } println(`Finished at $now()$`); } The main block records in-between advancing the clock by 1/4 (0.25).\nConverting Time Values To visualize times properly, they must be converted to a format that the visualization library expects.\nIn addition to the chosen offset (2020-04-01 in our case), we also need a scaling factor to convert the logical clock values of ABS to real date and time values. We choose to represent each day by an increment of 1; fractional values of the clock represent the time of day. Since our model advances the clock by 1/4 sixteen times, the values are recorded at 6am, 12pm, 6pm and midnight for four days.\nAs an example, here is a Javascript function that takes the startdate (as a string parseable via new Date) and offset (as a floating point number, with the integer part the number of days and the fractional part the time of day, with 0.5 exactly noon) and returns a Javascript Date object.\nfunction absolute_date(startdate, offset) { let days = Math.floor(offset); let time = offset - days; let date = new Date(startdate); date.setDate(date.getDate() + days); date.setTime(date.getTime() + time * 24 * 60 * 60 * 1000); return date; } Visualizing the Time Series The following is a complete HTML file that uses the Highcharts library to draw a line diagram of the random values generated by ABS. The function drawChart retrieves the starting offset and value list via the Model API, then creates a Highcharts chart with the downloaded values.\n\u003c!DOCTYPE HTML\u003e \u003chtml\u003e \u003chead\u003e \u003cmeta http-equiv=\"Content-Type\" content=\"text/html; charset=utf-8\"\u003e \u003ctitle\u003eDate and Time in ABS\u003c/title\u003e \u003cscript src=\"https://ajax.googleapis.com/ajax/libs/jquery/3.4.1/jquery.min.js\"\u003e\u003c/script\u003e \u003cscript src=\"https://code.highcharts.com/highcharts.js\"\u003e\u003c/script\u003e \u003cscript src=\"https://code.highcharts.com/modules/exporting.js\"\u003e\u003c/script\u003e \u003cscript src=\"https://code.highcharts.com/modules/export-data.js\"\u003e\u003c/script\u003e \u003c/head\u003e \u003cbody\u003e \u003ch1\u003eDate and Time in ABS\u003c/h1\u003e \u003cdiv id=\"chart-container\"\u003e \u003c/div\u003e \u003cscript type=\"text/javascript\"\u003e 'use strict'; function absolute_date(startdate, offset) { let days = Math.floor(offset); let time = offset - days; let date = new Date(startdate); date.setDate(date.getDate() + days); date.setTime(date.getTime() + time * 24 * 60 * 60 * 1000); return date.getTime(); // number of milliseconds, as needed by Highcharts } function drawChart(){ $.when( $.getJSON(\"/call/Calendar/getStartDate\"), $.getJSON(\"/call/Calendar/getValues\") ).done(function(resstartdate, resvalues) { let startdate = resstartdate[0].result; let data = resvalues[0].result.map(p =\u003e [absolute_date(startdate, p.fst), p.snd]); Highcharts.chart('chart-container', { type: 'line', title: { text: 'Dates and values from ABS' }, xAxis: { type: 'datetime' }, yAxis: { title: { text: 'Value (random number)' } }, series: [{ name: 'random value', data: data }] }); }); } $(document).ready(function(){ drawChart(); }); \u003c/script\u003e \u003c/body\u003e \u003c/html\u003e Running the Example The following small Makefile can be used to compile and start the model. Make sure to store the ABS model in a file CalendarTime.abs and the html in a file index.html, then type make run and connect the browser to http://localhost:8080.\n.PHONY: all all: run\t## Generate data and start model (default) .PHONY: compile compile: CalendarTime.abs index.html ## Compile the model absc --erlang CalendarTime.abs --modelapi-index-file index.html .PHONY: compile run: compile\t## Execute the model gen/erl/run -p 8080 -v .PHONY: help help:\t## Display this message @grep -E '^[a-zA-Z_-]+:.*?## .*$$' $(MAKEFILE_LIST) | sort | awk 'BEGIN {FS = \":.*?## \"}; {printf \"\\033[36m%-30s\\033[0m %s\\n\", $$1, $$2}'",
    "description": "An example for using Real-Time ABS to calculate with real (calendar) dates and times and visualize them on a graphical timeline.",
    "tags": [],
    "title": "Modeling and Visualizing Calendar Time",
    "uri": "/documentation/examples/time-and-date/index.html"
  },
  {
    "breadcrumb": "The ABS Language \u003e Documentation \u003e Tutorials",
    "content": "General Overview We prototype a static analysis technique that computes upper bounds of virtual machine usages in a dialect of ABS, called vml, whose syntax will be covered by the examples in this tutorial, with explicit acquire and release operations of virtual machines. In our language it is possible to delegate other (ad-hoc or third party) concurrent code to release virtual machines (by passing them as arguments of invocations). Our technique is modular and consists of (i) a type system associating programs with behavioural types that records relevant information for resource usage (creations, releases, and concurrent operations), (ii) a translation function that takes behavioural types and return cost equations. It is integrated with the solver CoFloCo that given the cost equations produces the result.\nResource Analysis In this section we present how to compute the cost of a vml program in term of virtual machine usage.\nFirst, select Resource Analysis (SRA) from the pull-down menu at the top of the window on the center-left. The parameters of the selected analysis are automatically set, so there is nothing to be configured in the Settings section in the top-left corner.\nAs an example, open the program doubleRelease.vml :\n/* DOUBLE RELEASE */ Int doubleRelease(VM x, VM y) { release x; release y; return 0 ; } Int user1() { VM x ; VM y ; Fut\u003cInt\u003e f ; x = new VM() ; y = new VM(); f = this!doubleRelease(x, y); Int a = f.get ; return 0 ; } { Fut\u003cInt\u003e fuser1 = this!user1(); Int a = fuser1.get; } Let us analyze the program. Click on Run to perform the analysis.\nThe output of the analysis is shown in three tabs of the console, which are generated by the tool:\nTypes contains the behavioural types generated for the input program Equations contains the cost equations resulted by the translation of the behavioural types UBs which is the overall output and shows the upper bounds. For the doubleRelease.vml we get: ### Partitioned upper bound of main(MAINVM): * 2 if [] ### Partitioned upper bound of doubleRelease012net(THISVM,X,Y): * -2 if [THISVM=1,X=1,Y=1] * -1 if [THISVM=1,X=1,Y\u003e=2] or [THISVM=1,Y=1,X\u003e=2] * 0 if [THISVM=1,X\u003e=2,Y\u003e=2] or [THISVM=3] ### Partitioned upper bound of user10net(THISVM): * 0 if [3\u003e=THISVM,THISVM\u003e=1] ### Partitioned upper bound of doubleRelease012peak(THISVM,X,Y): * 0 if [X=1,Y=1,2\u003e=THISVM] * 0 if [X=1,2\u003e=THISVM,Y\u003e=2] or [Y=1,2\u003e=THISVM,X\u003e=2] or [X=1,2\u003e=THISVM,0\u003e=Y] * 0 if [2\u003e=THISVM,X\u003e=2,Y\u003e=2] or [2\u003e=THISVM,0\u003e=Y,X\u003e=2] or [3\u003e=THISVM,0\u003e=X] or [THISVM=3,X\u003e=1] ### Partitioned upper bound of user10peak(THISVM): * 0 if [THISVM=3] * 2 if [2\u003e=THISVM]",
    "description": "We prototype a static analysis technique that computes upper bounds of virtual machine usages in a dialect of ABS called vml.",
    "tags": [],
    "title": "Resource Analysis with SRA",
    "uri": "/documentation/tutorials/sra/index.html"
  },
  {
    "breadcrumb": "The ABS Language",
    "content": "We welcome bug reports and feature requests submitted via github at https://github.com/abstools/abstools/issues.\nTo contact the maintainers, post on the discussion form at https://github.com/abstools/abstools/discussions or write to abs-info@abs-models.org.\nYou can subscribe to the developers’ mailing list at the developer list manager page, or subscribe to a low-traffic announcement-only list at the announcement list manager page.",
    "description": "We welcome bug reports and feature requests submitted via github at https://github.com/abstools/abstools/issues.\nTo contact the maintainers, post on the discussion form at https://github.com/abstools/abstools/discussions or write to abs-info@abs-models.org.\nYou can subscribe to the developers’ mailing list at the developer list manager page, or subscribe to a low-traffic announcement-only list at the announcement list manager page.",
    "tags": [],
    "title": "Contact",
    "uri": "/contact/index.html"
  },
  {
    "breadcrumb": "The ABS Language \u003e Documentation \u003e Examples",
    "content": "The Model API of ABS lets us display information in various ways. This example shows how to display geo-annotated ABS data on a map. To display the map in a browser, we use OpenStreetmap via the Leaflet library.\nThe complete code for this example can be found at https://github.com/abstools/absexamples/tree/master/collaboratory/examples/gis-modeling/.\nCoordinates in ABS In OpenStreetmap, coordinates are given as a (lat, long) pair of floating-point numbers. We model map data as MapData(Float lat, Float long, String description), which is then returned via the Model API. The complete code of the ABS part is as follows:\nmodule MapObjects; data MapData = MapData(Float lat, Float long, String description); interface OMap { [HTTPCallable] Pair\u003cFloat, Float\u003e getInitialCoordinates(); [HTTPCallable] List\u003cMapData\u003e getMapObjects(); } class OMap implements OMap { Pair\u003cFloat, Float\u003e getInitialCoordinates() { return Pair(59.90, 10.73); } List\u003cMapData\u003e getMapObjects() { return list[MapData(59.91115, 10.7357, \"City Hall\"), MapData(59.90758, 10.75197, \"Opera House\")]; } } { [HTTPName: \"map\"] OMap m = new OMap(); } Accessing and displaying coordinates When the running model is accessed via a browser, the createMap function in the model’s index.html file is called. This function creates a map, sets its initial location according to the getInitialCoordinates method (Lines 6-12), then adds the objects returned by the getMapObjects method (Lines 14-17). Both of these ABS methods are called from JavaScript code in createMap (Lines 2, 3).\n1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 function createMap() { Promise.all([fetch(\"/call/map/getInitialCoordinates\"), fetch(\"/call/map/getMapObjects\")]) .then((values) =\u003e values.map(p =\u003e p.json())).then((p) =\u003e Promise.all(p)) .then(([coords, objects]) =\u003e { var mymap = L.map('mapid').setView([coords.result.fst, coords.result.snd], 13); L.tileLayer('https://{s}.tile.openstreetmap.org/{z}/{x}/{y}.png', { maxZoom: 19, attribution: '\u0026copy; \u003ca href=\"https://openstreetmap.org/copyright\"\u003eOpenStreetMap contributors\u003c/a\u003e' }).addTo(mymap); L.control.scale().addTo(mymap); objects.result.forEach(item =\u003e L.marker([item.lat, item.long]) .addTo(mymap) .bindPopup(item.description)); var popup = L.popup(); function onMapClick(e) { popup.setLatLng(e.latlng) .setContent(\"You clicked the map at \" + e.latlng.toString()) .openOn(mymap); } mymap.on('click', onMapClick); }); } Running the Example Since the model includes a custom html page and support library, the compiler needs to run with the --modelapi-index-file and --modelapi-static-dir arguments. See the Makefile for the commands to compile and run the example on the Erlang or Java backend.\nAfter starting the model, the map can be accessed at http://localhost:8080.",
    "description": "An example on how to display data from ABS on a map via the Model API",
    "tags": [],
    "title": "Displaying geo-annotated information",
    "uri": "/documentation/examples/gis-modeling/index.html"
  },
  {
    "breadcrumb": "The ABS Language \u003e Documentation \u003e Examples",
    "content": "This example shows a model of a small cyber-physical system consisting of a water tank with faucet and drain, and a controller opening and closing the exit valve of the drain. The model illustrates discrete-event simulation, timed semantics, and custom visualization in ABS.\nThe complete code can be found at https://github.com/abstools/absexamples/tree/master/collaboratory/examples/single-watertank/\nModeling a Water Tank The following class shows the model of a water tank. The field level holds the current water level, the field valve_open records the status of an exit valve (open or not open).\nThe water tank has active behavior. The run method calculates the new water level on every time tick: fillrate is always added to the current level (water is always flowing in), and the level decreases by drainrate * level in case the valve is open, since water pressure is proportional to the water level.\nmodule SingleWaterTank; data ValveCommand = Open | Close; interface WaterTank { Float getLevel(); Unit valvecontrol(ValveCommand command); [HTTPCallable] List\u003cPair\u003cInt, Float\u003e\u003e getValveAndLevelHistory(); } class WaterTank(Float fillrate, Float drainrate) implements WaterTank { Float level = 0.0; Bool valve_open = False; List\u003cPair\u003cInt, Float\u003e\u003e history = list[]; List\u003cPair\u003cInt, Float\u003e\u003e getValveAndLevelHistory() { return reverse(history); } Float getLevel() { return level; } Unit valvecontrol(ValveCommand command) { valve_open = command == Open; } Unit run() { while (True) { await duration(1, 1); // Water inflow is constant, water outflow is // proportional to the current tank level level = level + fillrate; if (valve_open) { level = max(0.0, level - drainrate * level); } history = Cons(Pair(when valve_open then 1 else 0, level), history); } } } The tank also holds the history of current level and valve status in the field history. The method getValveAndLevelHistory is annotated to be callable via the Model API, and will be used to visualize the tank level over time.\nModeling the Controller The task of the controller is to open and close a tank’s valve to keep the water level in a safe range. The controller object does not have any methods but is an active object as well. Its run method checks the tank’s water level once per clock cycle, and sends Open and Close commands as necessary.\ninterface Controller { } class Controller(WaterTank tank, Float minlevel, Float maxlevel) implements Controller { Unit run() { while (True) { Float level = await tank!getLevel(); if (level \u003e= maxlevel) { tank!valvecontrol(Open); } else if (level \u003c= minlevel) { tank!valvecontrol(Close); } await duration(1, 1); } } } { [HTTPName: \"watertank\"] WaterTank tank = new WaterTank(1.0, 0.2); Controller controller = new Controller(tank, 5.0, 10.0); } We also see, at the bottom, the main block that creates a water tank object, makes it visible to the Model API, and creates a controller object.\nVisualizing the Water Level over Time The visualization uses the Highcharts visualization library, so needs an online connection to work.\nWhen connecting e.g. to localhost:8080, the browser will make a connection to /call/watertank/getValveAndLevelHistory, which results in a call to the getValveAndLevelHistory method of the water tank. The returned data is then converted into two lists of values which are passed to Highchart to be plotted.\n\u003c!DOCTYPE HTML\u003e \u003chtml\u003e \u003chead\u003e \u003cmeta http-equiv=\"Content-Type\" content=\"text/html; charset=utf-8\"\u003e \u003ctitle\u003eWatertank\u003c/title\u003e \u003cscript src=\"https://code.highcharts.com/highcharts.js\"\u003e\u003c/script\u003e \u003cscript src=\"https://code.highcharts.com/modules/exporting.js\"\u003e\u003c/script\u003e \u003cscript src=\"https://code.highcharts.com/modules/export-data.js\"\u003e\u003c/script\u003e \u003c/head\u003e \u003cbody\u003e \u003ch1\u003eWatertank\u003c/h1\u003e \u003cdiv id=\"chart-container\"\u003e \u003c/div\u003e \u003c/body\u003e \u003cscript type=\"text/javascript\"\u003e 'use strict'; function drawChart() { fetch(\"/call/watertank/getValveAndLevelHistory\") .then(response =\u003e response.json()) .then(data =\u003e { let valvestatus = data.result.map(p =\u003e p.fst); let waterlevel = data.result.map(p =\u003e p.snd); Highcharts.chart('chart-container', { type: 'line', title: { text: 'Watertank' }, series: [ { name: 'valve status', data: valvestatus, step: 'right' }, { name: 'water level', data: waterlevel } ] }); }); } document.addEventListener(\"DOMContentLoaded\", function () { drawChart(); }); \u003c/script\u003e \u003c/html\u003e Running the Example As mentioned, the code of this example resides at https://github.com/abstools/absexamples/tree/master/collaboratory/examples/single-watertank/. Place the files Watertank.abs, index.html and Makefile into the same directory and run the command make to compile and start the model. Then, connect a browser to the URL http://localhost:8080/ to see the resulting graph. The resulting plot shows the water level decreasing when the valve is open, and increasing again when the valve is closed.",
    "description": "An example for discrete-time simulation of a simple physical system and controller using Real-Time ABS.",
    "tags": [],
    "title": "Modeling and Visualizing A Water Tank Controller",
    "uri": "/documentation/examples/single-watertank/index.html"
  },
  {
    "breadcrumb": "The ABS Language",
    "content": "Projects The development of the ABS language and tools has been supported by a number of research projects supported by the European Commission and the Research Council of Norway:\nHATS: Highly Adaptive and Trustworthy Software using Formal Methods Envisage: Engineering Virtualized Services HyVar: Scalable Hybrid Variability SIRIUS: Enabling digitalization in and beyond the oil and gas industry Contributors The following people have contributed to the ABS language and tools so far:\nElvira Albert Ade Azurat Nikolaos Bezirgiannis Joakim Bjørk Frank de Boer Richard Bubel Dave Clarke Jesús Correas Ferruccio Damiani Crystal Chang Din Antonio Flores-Montoya Abel Garcia Samir Genaim Elena Giachino Miguel Gómez-Zamalloa Georg Göri Stijn de Gouw Reiner Hähnle Einar Broch Johnsen Eduard Kamburjan Ivan Lanese Cosimo Laneve Michael Lienhardt Kelly Lin Enrique Martin-Martin Jacopo Mauro Radu Muschevici Behrooz Nobakht Olaf Owe Björn Petersen Germán Puebla Violet Ka I Pun Guillermo Román-Díez Ina Schaefer Rudi Schlatte Vlad Serbanescu Faiza Shehzad Oliver Stahl Martin Steffen Volker Stolz S. Lizeth Tapia Tarifa Lars Tveito Peter Y.H. Wong Ingrid Chieh Yu Miky Zamalloa Gianluigi Zavatarro",
    "description": "Projects The development of the ABS language and tools has been supported by a number of research projects supported by the European Commission and the Research Council of Norway:",
    "tags": [],
    "title": "Acknowledgments",
    "uri": "/acknowledgments/index.html"
  },
  {
    "breadcrumb": "The ABS Language \u003e Documentation \u003e Examples",
    "content": "This example shows a high-level model of a typical three-layer system serving client requests. The components are one load balancer, multiple web workers and an underlying database server. The model also contains one or more clients, which send requests to the load balancer.\nThe complete code to this example can be found here: https://github.com/abstools/absexamples/blob/master/collaboratory/examples/resource-modeling/\nThe basic architecture is as follows:\nExample structure The Loadbalancer class receives incoming messages from clients, chooses a Webworker object and routes the request to it. The worker, in turn, calls the query method of the Database instance, then returns a result to the client via the load balancer.\nFunctional Model without Resources The ABS model discussed in this section is here: basic-model-no-resources.abs\nWe use a basic model to implement the control flow of a typical web request, skipping any application logic. Clients access the service by calling processRequest() on a LoadBalancer isntance which keeps a pool of Webworker components. All of them access the same Database object. The interface structure is as follows:\ninterface Database { String query(); } interface Webworker { String processRequest(); } interface Loadbalancer { String processRequest(); } Note that there is no interface for clients, since they do not expose any methods to call from the outside.\nWe abstract away from most of the processing and are only concerned with control flow, so the Database implementation returns a constant string:\nclass Database implements Database { String query() { return \"Result\"; } } In the same vein, the Webworker class models database communication and local processing:\nclass Webworker(Database db) implements Webworker { String processRequest() { String result = await db!query(); return result + \" from \" + toString(this); } } The class LoadBalancer fills its pool of Webworker instances on startup, and routes requests to a free webworker:\nclass Loadbalancer(Int nWorkers, Database db) implements Loadbalancer { List\u003cWebworker\u003e workers = Nil; Unit run() { Int i = 0; while (i \u003c nWorkers) { Webworker w = new Webworker(db); workers = Cons(w, workers); i = i + 1; } } String processRequest() { await length(workers) \u003e 0; Webworker w = head(workers); workers = tail(workers); String result = await w!processRequest(); workers = appendright(workers, w); return result; } } Each Client instance sends one request per time unit to the LoadBalancer from its run method:\nclass Client (Loadbalancer lb) { Unit run() { while (timeValue(now()) \u003c 100) { String s = await lb!processRequest(); println(s + \" at \" + toString(now())); await duration(1, 1); } } } Finally, the main block sets up and starts the model.\n{ Database db = new Database(); Loadbalancer lb = new Loadbalancer(5, db); new Client(lb); await duration(100, 100); } Adding Resources to the Model The ABS model discussed in this section is here: basic-model-resources-v1.abs\nWe now add resource locations and resource consumption to the model of the previous section.\nThe basic idea is to create objects at resource-carrying locations (see Deployment Components). DeploymentComponent is a pre-defined ABS class that models a virtual machine, or in general a location that supplies computation resources to the cogs running on it.\nSpecific parts of the code are annotated with resource costs. Executing these code parts consumes resources, and execution is delayed when the location has run out of resources. Resources are refreshed periodically.\nThe interesting point is that adding deployment and cost information to an ABS model can be done piecemeal, and is minimally invasive.\nExample structure, with deployment components In the updated example, we deploy the Webworker and Database objects on a deployment component each. Note that we do not have to add a deployment component to every new object; we can leave some parts unspecified or abstract. Note that in the example, we make use of the CloudProvider class from the standard library, but deployment components can be directly created as well.\nIn the main block, we create a CloudProvider instance, tell it which instance types are available, and use it to create a deployment component for running the database on. The [DC: database_c] annotation creates the fresh Database object on that deployment component.\n{ CloudProvider provider = new CloudProvider(\"Amazon\"); provider!setInstanceDescriptions(map[Pair(\"Small\", map[Pair(Cores, 1), Pair(Speed, 15)])]); DeploymentComponent database_c = await provider!launchInstanceNamed(\"Small\"); [DC: database_c] Database db = new Database(); Loadbalancer lb = new Loadbalancer(5, db, provider); new Client(lb); await duration(100, 100); provider!shutdown(); } The LoadBalancer uses the same CloudProvider instance to create the web workers:\nclass Loadbalancer(Int nWorkers, Database db, CloudProvider provider) implements Loadbalancer { List\u003cWebworker\u003e workers = Nil; Unit run() { Int i = 0; while (i \u003c nWorkers) { DeploymentComponent dc = await provider!launchInstanceNamed(\"Small\"); [DC: dc] Webworker w = new Webworker(db); workers = Cons(w, workers); i = i + 1; } } // All other code unchanged ... } The Database and Webworker classes now consume resources when processing requests. Each query call consumes a constant 3 Speed resources from the database’s deployment component, each processRequest call to a web worker consumes 16 resources from the web worker’s deployment component.\nclass Database implements Database { String query() { [Cost: 3] return \"Result\"; } } class Webworker(Database db) implements Webworker { String processRequest() { [Cost: 16] String result = await db!query(); return result + \" from \" + toString(this); } } To run the model on the Java backend, execute the following:\nabsc --java basic-model-resources-v1.abs -o basic-model-resources-v1.jar java -jar basic-model-resources-v1.jar -p 8080 Then, open a browser to the address http://localhost:8080. The output will look similar to this (scroll down in the model API browser output to see more deployment components):\nScreenshot of resource consumption over time of the database and 3 webworkers, round-robin scheduling We can see that all deployment components are lightly loaded, and that the load balancer distributes tasks in a round-robin strategy. Since the deployment component has a Speed capacity of 15 but the cost of one processRequest execution is 16, each request takes two time units.\nChanging Load Balancing Strategies The ABS model discussed in this section is here: basic-model-resources-v2.abs\nWith a one-line change in the load balancer, we can model a different load balancing strategy: we switch from round-robin to a LIFO (stack-based) strategy.\nString processRequest() { await length(workers) \u003e 0; Webworker w = head(workers); workers = tail(workers); String result = await w!processRequest(); workers = Cons(w, workers); return result; } To run the model on the Java backend, execute the following:\nabsc --java basic-model-resources-v2.abs -o basic-model-resources-v2.jar java -jar basic-model-resources-v2.jar -p 8080 Then, open a browser to the address http://localhost:8080. The output will look similar to this (scroll down in the model API browser output to see more deployment components):\nScreenshot of resource consumption over time of the database and 2 webworkers, with LIFO scheduling of the load balancer It can be seen that one web worker is enough to carry the load of the given client scenario; all web workers except the first one are idle over the course of the simulation.\nChanging the Client Load Scenario The ABS model discussed in this section is here: basic-model-resources-v3.abs\nThe previous examples showed a load scenario where most machines are idle. We can add more clients to simulate a higher load, with the following main block:\n{ CloudProvider provider = new CloudProvider(\"Amazon\"); provider!setInstanceDescriptions(map[Pair(\"Small\", map[Pair(Cores, 1), Pair(Speed, 15)])]); DeploymentComponent database_c = await provider!launchInstanceNamed(\"Small\"); [DC: database_c] Database db = new Database(); Loadbalancer lb = new Loadbalancer(5, db, provider); new Client(lb); new Client(lb); new Client(lb); new Client(lb); new Client(lb); new Client(lb); new Client(lb); new Client(lb); new Client(lb); await duration(100, 100); provider!shutdown(); } To run the model on the Java backend, execute the following:\nabsc --java basic-model-resources-v3.abs -o basic-model-resources-v3.jar java -jar basic-model-resources-v3.jar -p 8080 Then, open a browser to the address http://localhost:8080. The output will look similar to this (scroll down in the model API browser output to see more deployment components):\nScreenshot of resource consumption over time of the database and 2 webworkers, with increased client load In this last example, the database server is running at approximately 50% load, and all 5 web workers are running near capacity.\nFurther Possibilities for Resource Modeling Note that the scenarios presented above are somewhat static, but that does not need to be the case:\nWe can dynamically add deployment components and add and remove worker objects; this can be used to model redeployment at runtime Cost annotations can be any ABS expression over local variables and class fields that produces a number; this can be used to model varying costs of message processing, either stochastic or as a function of the message payload The resources available to a deployment component can be increased and decreased; this can be used to model stochastic machine performance decrease, or resource transfer between machines",
    "description": "An example on how to model distributed application deployments",
    "tags": [],
    "title": "Modeling Resources",
    "uri": "/documentation/examples/resource-modeling/index.html"
  },
  {
    "breadcrumb": "The ABS Language \u003e Documentation \u003e Examples",
    "content": "A multicore memory system consists of cores that contain tasks to be executed, the data layout in main memory (indicating where data is allocated), and a system architecture consisting of cores with private multi-level caches and shared memory (see Figure 1). Such a system is parametric in the number of cores, the number and size of caches, and the associativity and replacement policy. Data is organised in blocks that move between the caches and the main memory. For simplicity, we abstract from the data content of the memory blocks, assume that the size of cache lines and memory blocks in main memory coincide and transfer memory blocks from the caches of one core to the caches of another core via the main memory. As a consequence, the tasks executed in the cores are represented as data access patterns, abstracting from their computational content.\nThe complete code can be found at https://github.com/abstools/absexamples/tree/master/collaboratory/case_studies/Multicore_Model/\nFigure 1: System memory architecture Task execution on a core requires memory blocks to be transferred from the main memory to the closest cache. Each cache has a pool of instructions to move memory blocks among caches and between caches and main memory. Memory blocks may exist in multiple copies in the memory system. Consistency between different copies of a memory block is ensured using the standard cache coherence protocol MSI, with which a cache line can be either modified, shared or invalid. A modified cache line has the most recent value of the memory block, therefore all other copies are invalid (including the one in main memory). A shared cache line indicates that all copies of the block are consistent. The protocol’s messages are broadcasted to the cores. Following standard nomenclature, Rd messages request read access and RdX messages read exclusive access to a memory block. The latter invalidates other copies of the same block in other caches to provide write access.\nFigure 2: ABS model structure This use-case contains a distributed implementation of this model in ABS (see Figure 2). A transition system specification of this model can be found at https://doi.org/10.1016/j.scico.2019.04.003\nWe have two versions of the model which can run with different initial configurations:\nwithoutPenaltiesSimplified: no collection of penalties withPenaltiesSimplified: collection of hits and penalties. Hits count the number of times a memory block was found in the caches. Penalties vary (from 1,10, 100, etc.) depending from where in the memory system the memory block was accessed. The further down the data is accessed in the memory system, the higher the penalty. Model configurations All the configurations have 4 cores with three levels of caches, but they are varying in the number, size and access patterns of the tasks.\nConfig1:\nContains 10 tasks with 100 read/write instructions each. It has one access per memory block, where all the tasks do not share any block during execution.\nConfig2:\nContains 10 tasks with 100 read/write instructions each. Tasks interleaves between a read and a write with one access per memory block. Each task shares with the next task 1/4 of its blocks.\nConfig3:\nContains 10 tasks with 100 read/write instructions each. Task interleaves between a read and a write to the same memory block, therefore each task has two accesses read/write per memory block. All the tasks do not share any block between them during execution.\nConfig4:\nContains 10 identical tasks with a loop accessing one memory block many times. Since all the cores access a single memory block many times, the execution generates congestion.\nRunning the simulation with penalties absc --erlang common/*.abs withPenalties/*.abs configs/ConfigX.abs ./gen/erl/run Where X correspond to which initial configuration is chosen.\nExample output of running Config4:\nC1: hits = 10; penalties = 120 C2: hits = 10; penalties = 1220 C3: hits = 10; penalties = 2210 C4: hits = 10; penalties = 3090 Running the simulation without penalties absc --erlang common/*.abs withoutPenalties/*.abs configs/ConfigX.abs ./gen/erl/run Example output of running Config1:\nExecution has terminated",
    "description": "A model of the MSI cache coherency protocol.",
    "tags": [],
    "title": "ABS Model of a Multicore Memory System",
    "uri": "/documentation/examples/multicore_memory/index.html"
  },
  {
    "breadcrumb": "The ABS Language",
    "content": "The Collaboratory is a browser-based IDE for ABS that offers an online, zero install version of the ABS toolchain. Use it to experiment with the language in a risk-free environment.\nLoad our ready-made examples or run your own ABS models. The editor has many features of an IDE, including showing you an outline of the code, and of course reporting syntax- and type errors.\nThe collaboratory also supports many of the analysis tools that we have developed, like COSTA and SACO.\nA collaboratory instance is hosted online at http://ei.abs-models.org:8082/clients/web/. Please use this instance responsibly, and consider running the collaboratory on your local machine.\nTo run a private local instance of the collaboratory, see Running a Browser-Based IDE.",
    "description": "The Collaboratory is a browser-based IDE for ABS that offers an online, zero install version of the ABS toolchain. Use it to experiment with the language in a risk-free environment.\nLoad our ready-made examples or run your own ABS models. The editor has many features of an IDE, including showing you an outline of the code, and of course reporting syntax- and type errors.\nThe collaboratory also supports many of the analysis tools that we have developed, like COSTA and SACO.",
    "tags": [],
    "title": "The Collaboratory",
    "uri": "/laboratory/index.html"
  },
  {
    "breadcrumb": "",
    "content": "The ABS Language ABS is a language for Abstract Behavioral Specification, which combines implementation-level specifications with verifiability, high-level design with executablity, and formal semantics with practical usability. ABS is a concurrent, object-oriented, modeling language that features functional data-types.\nABS is designed to develop executable models with an object-oriented program flow ABS targets distributed and concurrent systems by means of concurrent object groups and asynchronous method calls ABS supports model variability based on delta-oriented specifications ABS supports deployment modelling based on high-level deployment models ABS supports a range of techniques for model exploration and analysis, based on formal semantics Overview\nGetting Started\nThe Language Manual\nExamples\nTutorials\nPublications\nContact\nAcknowledgments",
    "description": "The ABS Language ABS is a language for Abstract Behavioral Specification, which combines implementation-level specifications with verifiability, high-level design with executablity, and formal semantics with practical usability. ABS is a concurrent, object-oriented, modeling language that features functional data-types.\nABS is designed to develop executable models with an object-oriented program flow ABS targets distributed and concurrent systems by means of concurrent object groups and asynchronous method calls ABS supports model variability based on delta-oriented specifications ABS supports deployment modelling based on high-level deployment models ABS supports a range of techniques for model exploration and analysis, based on formal semantics Overview",
    "tags": [],
    "title": "The ABS Language",
    "uri": "/index.html"
  },
  {
    "breadcrumb": "The ABS Language",
    "content": "",
    "description": "",
    "tags": [],
    "title": "Categories",
    "uri": "/categories/index.html"
  },
  {
    "breadcrumb": "The ABS Language",
    "content": "",
    "description": "",
    "tags": [],
    "title": "Tags",
    "uri": "/tags/index.html"
  }
]