Modeling from A to Z/Modeling the Waste Management System

From Wikibooks, open books for an open world
Jump to navigation Jump to search

Next Generation Nuclear Power Stations and Waste Management[edit | edit source]

It would appear that the Nuclear Power Station will be with us for the foreseeable future. Moreover, it is not so much the generation of electricity that matters but the management of the waste that results.

Waste management is not unique to the domain of nuclear power. The current need for a green revolution to undercut climate change and global warming depends crucially on how oil-related products such as plastics are re-cycled or incinerated. Illegal dumping is rife in many countries.

In this section we look at one aspect of waste management, adopted from the nuclear industry and show how it may be re-used for general waste management. In itself the development illustrate a general principle in (software) process improvement. Real systems evolve and migrate. They are very rarely begun from scratch. Any software development plan ought to follow the same process improvement of the system to match.

Tracking is just like searching. It relies on addresses. And now know that addressing may be a matter of placing cookies or RFID tagging.

Sources of inspiration[edit | edit source]

We will begin our model by looking at some work already published. That is to say, we will not pretend any originality or creativeness. Our starting point will be a “tracking manager study” (TMS)[1] which was carried out as part of the «Research Study into the use of Computer-based Tracking Systems as valuable support to Safety Cases in Nuclear Power Technology»[2]

In essence there are two kinds of things: containers and what goes into them. The different kinds of containers are easy to point out. In the TMS[3] there are 5 of them:

We already know from our earlier work on Alloy that we can introduce an abstract signature for Container and introduce the 5 container types as extensions:

abstract sig Container {}
sig Crate, Package, Liner, Puck, Drum extends Container {}

Those things that go into certain kinds of containers may be called materials. In our first study of the TMS we will look at just 4 material types[6]:

  • glass
  • plastic
  • metal
  • liquor

Just as for Container above, so we introduce an abstract signature for Material and the four types of material then become extensions:

abstract sig Material {}
sig Glass, Plastic, Metal, Liquor extends Material {}

Finally, for this introduction, one notes that the phases of processing within the Waste Management System can be classified analogously:

abstract sig Phase {}
sig Unpacking, Sorting, Assaying, Compacting, Exporting extends Phase {}

Instead of using the term "Phase", one might prefer "Process". Here is the list of Phases modelled:

  • Unpacking (crates)
  • Sorting (contents)
  • Assaying (materials)
  • Compacting (materials)
  • Exporting (stuff)

Alloy model of the Tracking Management System (TMS)[edit | edit source]

This is a re-modelling of the tracker system described in

  1. John Fitzgerald and Cliff Jones, 1998, pp.1-28
  2. John. S. Fitzgerald, 1999, pp.69-94
  3. John Fitzgerald and Peter Gorm Larsen, pp. 137-201?

Introductory text[edit | edit source]

A detailed formal model of a system is but one step away from implementation. That step consists of the working out of the formal mathematical expressions. Such working out is a mixture of hardware and software. Much of it will be off-the-shelf. Some of it will necessarily be hand crafted. But before we get to this stage of detail, we need an abstract bird's-eye view. This overview will capture everything in essence and will be comprehensible. Here is such an executive overview supported by Alloy.

System requirements[edit | edit source]

A Tracking Management System (TMS) monitors the position of containers of material as they pass through the various phases of processing in an industrial plant (IP) such as a waste management facility (WMF).

Each container holds only one type of material and can be in at most one processing phase at a time. Each processing phase has a maximum container capacity and can only accept certain types of materials.

System state[edit | edit source]

At any point in time a system state of the TMS must record:

  1. The catalog of material type contents of each container in the WMS. Briefly, this is the simply denoted by the cntCatalog
  2. The collection of containers in each processing phase.
  3. The phase properties of each processing phase:
    • the maximum container capacity (maxCapacity) and
    • the acceptable types of materials (mtrType).

System state constraints[edit | edit source]

At any point in time a system state of the TMS must satisfy the following system state constraints:

  1. Each container can hold at most one type of material. Each container can be in at most one processing phase at a given time. Each processing phase can have at most one value for it's maximum capacity.
  2. All processing phases have recorded phase properties: a maximum capacity and acceptable material types.
  3. Each processing phase in the industrial plant has a maximum capacity of at least one.
  4. The containers in any given processing phase all have recorded material contents.
  5. The active processing phases have recorded phase properties: a maximum capacity and acceptable material types.
  6. Each type of material in the IP has a possible processing phase.
  7. Each phase in the IP is operating within capacity.
  8. In any phase, all the containers in that phase have the expected kinds of materials inside them.

System operations[edit | edit source]

The TMS has a number of operations which modify the system state:

  1. initOp: specifies the properties of an initial state of the TMS.
  2. insertOp: adds a new container whose contents are of a given material type to the industrial plant container catalogue. (was introduce operation)
  3. remOp: removes a container from given phase of processing
  4. delOp: deletes a container from both the container content catalogue and the tracker system.
  5. permitOp: which decides whether a container may be moved into a given phase.
  6. moveOp: moves a container into a given phase processing within the tracker system.

Alloy module[edit | edit source]

module TrackingManagementSystem -- abbreviated TMS

open util/relation as rel -- Binary relation module.
open util/natural as nat -- Natural number module.
open util/boolean as bool -- Boolean module

sig Container, Material, Phase {} -- Containers, material types, and processing phases.

sig SystemState {

cntCatalog: Container -> Material, -- The container catalogue.

trkSystem: Container -> Phase, -- The tracker system.

maxCapacity: Phase -> Natural, -- Phase max capacity record.

mtrType: Phase -> Material -- Phase material types record.


Visualization[edit | edit source]

We know from earlier work on Alloy that this is sufficient information for us to visualise the structure of the metamodel:

The metamodel of the Tracking Management System projected over the SystemState

System constraints[edit | edit source]


pred FieldTypeCns(s: SystemState) {
    functional[sysState.cntCatalog, dom[sysState.cntCatalog]]
    functional[sysState.trkSystem, dom[sysState.trkSystem]]
    functional[sysState.maxCapacity, dom[sysState.maxCapacity]]
    dom[sysState.maxCapacity] = dom[sysState.mtrType]
    all phase: dom[sysState.maxCapacity] | sysState.maxCapacity[phase] != Zero


pred TrackerContainerCns(sysState: SystemState) {
    dom[sysState.trkSystem] in dom[sysState.cntCatalog]


pred TrackerPhaseCns(sysState: SystemState) {
    ran[sysState.trkSystem] in dom[sysState.maxCapacity]
    ran[sysState.trkSystem] in dom[sysState.mtrType]

A simpler waste management model[edit | edit source]

Containers[edit | edit source]

Let us begin with the container? Imagine that you are in a building where there are containers for

  • the disposal of empty water bottles,
  • used ink-jet cartridges,
  • used batteries, and
  • waste paper.

These containers are collected by the garbage firm NoWasteNoWant once a week and brought to the waste-management facility in the city.

Container notes[edit | edit source]

When we talk about "empty water bottles" we are thinking of either plastic or glass materials. For now, we will limit ourselves to just two types:

  • glass bottle
  • plastic bottle

Container Types[edit | edit source]

For the sake of the first model on waste management. We will assume there are just two types of container:

  • wet container — used for all liquid stuff, that is the plastic or glass bottles.
  • dry container — used for everything else

Notes[edit | edit source]

  1. TMS is our acronym. It stands for Tracking Manager Study. The use of acronyms in Computer Science is widespread. The habit is probably due to the very concept of programming variable. It would be nice to verify this hypothesis. We will use this acronym in our own model for the Waste Management System. But in this case, TMS will stand for Tracking Management System. Acronyms can be flexible, even if ambiguous.
  2. Fitzgerald&Jones 1998, p.28.
  3. Fitzgerald&Jones 1998, p.3
  4. The example of the Universal Puck at SLAC Stanford might give some idea of what sort of thing a puck is, what it might look like, and how it might be used.
  5. Report WSRC-MS-98-00571 gives a very good overview of nuclear waste management issues, including a very useful text on the use of the puck.
  6. Fitzgerald&Jones 1998, p.3.

References[edit | edit source]

Reading links[edit | edit source]

  1. Bicarregui, Juan Carlos (editor), (1988). Proof in VDM: case studies. London: Springer-Verlag. ISBN 978-3540761860. {{cite book}}: |first= has generic name (help); Cite has empty unknown parameter: |coauthors= (help)CS1 maint: extra punctuation (link)
  2. Fitzgerald, John (1998). "A Tracking System". In Bicarregui, Juan Carlos (ed.). Proof in VDM: Case Studies. London: London: Springer-Verlag. pp. 1–29. {{cite book}}: Cite has empty unknown parameter: |coeditors= (help); Unknown parameter |coauthors= ignored (|author= suggested) (help)

e-Links[edit | edit source]