Re: How to abstract a set?
- From: me@xxxxxxxxxxx (Jamie Andrews; real address @ bottom of message)
- Date: 30 Oct 2007 20:01:39 GMT
hbdere <hbdere@xxxxxxx> wrote:
this happens to me all the time when trying to abstract software - I
need to verify properties like 'only if a customer has been logged in,
he may retrieve something'. Because I want to do model checking, I
require a finite abstraction, so maintaining a set of customers logged
in is not feasible. A naive approach would be to distinguish the
abstract states 'the customer a is logged in' and '... not logged in',
and only talk about customer a. But then I need to make sure that the
abstract state 'a is logged in' is not reached by an action other than
a logging in etc., so to make this short: any literature on that
topic?
You might be interested in my work on log file analysis:
http://www.csd.uwo.ca/faculty/andrews/papers/tse03-lfa.ps.gz
One aspect of a possible solution would be to consider that you
have a class of state machines, where the unique identifier
("name") of the state machine is parameterized by the unique
identifier of the customer. I don't know if the log file
analysis stuff is directly applicable, but it might give you
some ideas for a solution.
--Jamie. (efil4dreN)
andrews .uwo } Merge these two lines to obtain my e-mail address.
@csd .ca } (Unsolicited "bulk" e-mail costs everyone.)
.
- References:
- How to abstract a set?
- From: hbdere
- How to abstract a set?
- Prev by Date: Re: Recursively enumerable sets
- Next by Date: CSR 2008: First Call for Papers
- Previous by thread: How to abstract a set?
- Next by thread: Reduction from Vertex Cover to SAT
- Index(es):
Relevant Pages
|
