411 REFERENCE · Wikibooks
Modeling from A to Z/Modeling the Waste Management System
Reference material by Wikibooks contributors. This retains its source identity and is not 411 news reporting.
Next Generation Nuclear Power Stations and Waste Management
waste management
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
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)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.
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»Fitzgerald&Jones 1998, p.28.
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 TMSFitzgerald&Jones 1998, p.3 there are 5 of them:
crate
package
liner
puckThe 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.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.
drum container
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:
<blockquote>
abstract sig Container {}
sig Crate, Package, Liner, Puck, Drum extends Container {}
</blockquote>
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 typesFitzgerald&Jones 1998, p.3.:
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:
<blockquote>
abstract sig Material {}
sig Glass, Plastic, Metal, Liquor extends Material {}
</blockquote>
Finally, for this introduction, one notes that the phases of processing within the Waste Management System can be classified analogously:
<blockquote>
abstract sig Phase {}
sig Unpacking, Sorting, Assaying, Compacting, Exporting extends Phase {}
</blockquote>
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)
This is a re-modelling of the tracker system described in
John Fitzgerald and Cliff Jones, 1998, pp.1-28
John. S. Fitzgerald, 1999, pp.69-94
John Fitzgerald and Peter Gorm Larsen, pp. 137-201?
Introductory text
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
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
At any point in time a system state of the TMS must record:
The catalog of material type contents of each container in the WMS.
Briefly, this is the simply denoted by the cntCatalog
The collection of containers in each processing phase.
The phase properties of each processing phase:
the maximum container capacity (maxCapacity) and
the acceptable types of materials (mtrType).
System state constraints
At any point in time a system state of the TMS must satisfy the following system state constraints:
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.
All processing phases have recorded phase properties:
a maximum capacity and
acceptable material types.
Each processing phase in the industrial plant has a maximum capacity of at least one.
The containers in any given processing phase all have recorded material contents.
The active processing phases have recorded phase properties:
a maximum capacity and
acceptable material types.
Each type of material in the IP has a possible processing phase.
Each phase in the IP is operating within capacity.
In any phase, all the containers in that phase have the expected kinds of
materials inside them.
System operations
The TMS has a number of operations which modify the system state:
initOp: specifies the properties of an initial state of the TMS.
insertOp: adds a new container whose contents are of a given material type to the industrial plant container catalogue.
(was introduce operation)
remOp: removes a container from given phase of processing
delOp: deletes a container from both the container content catalogue and the tracker system.
permitOp: which decides whether a container may be moved into a given phase.
moveOp: moves a container into a given phase processing within the tracker system.
Alloy module
module TrackingManagementSystem -- abbreviated TMS
<blockquote>
open util/relation as rel -- Binary relation module.
open util/natural as nat -- Natural number module.
open util/boolean as bool -- Boolean module
</blockquote>
sig Container, Material, Phase {} -- Containers, material types, and processing phases.
<blockquote>
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.
}
</blockquote>
Visualization
We know from earlier work on Alloy that this is sufficient information for us to visualise the
structure of the metamodel:
thumb|450px|center|The metamodel of the Tracking Management System projected over the SystemState
System constraints
[1]
<blockquote>
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
}
</blockquote>
[2]
<blockquote>
pred TrackerContainerCns(sysState: SystemState) {
dom[sysState.trkSystem] in dom[sysState.cntCatalog]
}
</blockquote>
[3]
<blockquote>
pred TrackerPhaseCns(sysState: SystemState) {
ran[sysState.trkSystem] in dom[sysState.maxCapacity]
ran[sysState.trkSystem] in dom[sysState.mtrType]
}
</blockquote>
A simpler waste management model
Containers
Container
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
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
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
2
References
Reading links
Bicarregui Juan Carlos (editor), Proof in VDM: case studies Springer-Verlag 1988 London 978-3540761860
John Fitzgerald Cliff B. Jones A Tracking System Proof in VDM: Case Studies Juan Carlos Bicarregui London: Springer-Verlag London 1-29 1998
e-Links
Nuclear power in France last access {2008-08-14}
Universal Puck last access {2008-08-14}
Report WSRC-MS-98-00571 Proposed New DOE Remote Facilities Overview - Designing for the Next Century last access {2008-08-15}
World Intellectual Property Organization (WIPO): (WO/2006/005905) METHOD FOR THE HANDLING AND MINIMISATION OF WASTE last access {2008-08-14}