parallel programming and specification tools
Eric ten Cate
We are looking for a parallel programming environment to support the
development of a large scale parallel numerical application for a
massively parallel system. Ideally we would like to have integrated
tools for (formal or semi-formal) specification of software, programming
in Fortran and/or C, and verification. The latter would include a proof
that the implementation is deadlockfree and does not suffer from starvation.
Note that we are not so much interested in parallellisation tools
(which help you make an existing sequential code parallel).
So far we have found CODE, PIE, POKER, MUPPET, PPSE and Integral. Only
the former two seem applicable. We have no reports of POKER and MUPPET
after 1988 and PPSE and Integral seem to be only in research stadium.
If there is anyone who can supply hints to other environments or who
has experience with any of the ones mentioned above, please send a note.
We have the feeling that so far, none of the environments truly supports
the formal specification of parallel software. Therefore, we are thinking
about having a separate environment for specification (the output of
which should preferably be usable in our programming environment). We are
considering RAISE and LOTOS. The latter seems to be aimed at the specification
of protocols and might therefore be less appropriate here.
Other specification methods that we considered are CSP, Unity and VDM, but
we did not come across any (stable) environment that supports the former two.
We welcome any notes about other specification tools for parallel
processing and about experience with any of them.
I will be happy to summarize the reactions to interested parties.
Regards,
Mark
------
Mark Roest Eric ten Cate
TWI/TA TWI/TA
Delft University of Technology Delft University of Technology
Mekelweg 4 Mekelweg 4
2628 CD DELFT 2628 CD DELFT
the Netherlands the Netherlands
ro...@dutind4.tudelft.nl ten...@dutind4.tudelft.nl
ten...@ph.tn.tudelft.nl
-------
Jeroen van de Lagemaat
|>
|>
|> If there is anyone who can supply hints to other environments or who
|> has experience with any of the ones mentioned above, please send a note.
|>
|> We have the feeling that so far, none of the environments truly supports
|> the formal specification of parallel software. Therefore, we are thinking
|> about having a separate environment for specification (the output of
|> which should preferably be usable in our programming environment). We are
|> considering RAISE and LOTOS. The latter seems to be aimed at the specification
|> of protocols and might therefore be less appropriate here.
|>
|> Other specification methods that we considered are CSP, Unity and VDM, but
|> we did not come across any (stable) environment that supports the former two.
|>
|> We welcome any notes about other specification tools for parallel
|> processing and about experience with any of them.
|>
|> I will be happy to summarize the reactions to interested parties.
|>
|>
|>
|>
The myth about LOTOS keeps popping-up!
What is LOTOS really? Language Of Temporal Ordening Specification is a
description technique based on the temporal ordening of observational behaviour.
So what can be specified:
- events, i.e. actions performed at gates (IO points)
- ordening of events
- data involved in events
- structering of events in processes
- hiding of events
- etc.., see ISO 8807!
What can be done with it:
- specification of systems at several levels, i.e. from user-requirements
to description of implementations, using different specification styles
How is it supported:
- Several tools have been developed to:
* write specs
* validate/verify specs
* compile specs to C, Ada
* transform specs, e.g. user-requirements in system architecture
Most of the tools have been incorporated in a coherent toolset (lite)
- At several countries centres of expertise are available (Spain, Italy, Germany
France, The Netherlands ...).
How is this possible:
The formal basis of LOTOS (formally defined syntax and semantics) allows both the unique
interpretation of specifications as well as building of the tools. Even these tools can be
tested for Conformance to the language.
Where does the myth come from:
LOTOS was developed within ISO as part of the work of JTC1 (TC97 in the past)
in SC21 (Information Processing Systems), the group responsible for OSI.
LOTOS was applied there mainly to communication protocols, e.g. Transport
Protocol and Service of OSI are described in LOTOS and published as Technical
Reports TR 10023 and 10024 last month.
Also, most of the work done in the area of Conformance Testing in ISO is now based on LOTOS.
What is it used for now? I know of the following applications:
- Manufacturing Control, design of a plant for CAD/CAM
- Safety regulations
- Space on-board systems
- Safety critical hard and software systems
- OSI protocols and ISDN protocols and end-systems
- Multi-media information systems
- ....
I challenge you: show me where LOTOS can not be applied succesfully!
NOTE: LOTOS does not all of the job, complementary methods and tools are needed
for succesful design and implementation of systems, not to forget the
designers creativity.
___
__/ \__________ Jeroen van de Lagemaat <lage...@cs.utwente.nl>
| \___/ |
|___ __ ___ | University of Twente
| | | / \ (__ | Tele-Informatics & Open Systems
| |__|__\__/____) | P.O. Box 217 NL-7500 AE Enschede The Netherlands
|_________________| tel. +31 53 893684 tfx. +31 53 333815
Humour, you're making me laugh.
- Herman Finkers, Dutch comedian -
Bonus, Iniquus, Celer - Delegitus Duo
[...]
>
> I challenge you: show me where LOTOS can not be applied succesfully!
> NOTE: LOTOS does not all of the job, complementary methods and tools are needed
> for succesful design and implementation of systems, not to forget the
> designers creativity.
postings.
Thanks
George Kambic
kam...@iccgcc.decnet.ab.com