An integration environment to put formal specifications into practical use in real-time systems
Pages 102 - 109
Abstract
This paper discusses several requirements to put formal specifications into practical use in real-time systems, and an integration environment called MENDELS ZONE to satisfy them. The integration environment includes algebraic specification, temporal logic, real-time Structured Analysis and Object-Oriented Design. It also defines a specification process that assists a designer in translating a specification developed with the real-time Structured Analysis method into an Object Oriented Design specification, and that finally generates Ada tasks. The specification process is defined to consist of several specification steps and several intermediate products. In order to validate the activity for each specification step, each intermediate product is described by two formal specification methods: algebraic specification and temporal logic.
References
[1]
{Booch86} C. Booch, Object-Oriented Development, IEEE Trans. Software Eng., Vol. SE-12, No. 12, 1986
[2]
{Docker89} T. W. G. Docker, Flexibility and Rigour in Structured Analysis, IFIP'89, 1989
[3]
{Folkjar80} P. Folkjar and D. Bjorner, A Formal Model of a generalized CSP-like language, IFIP'80, 1980
[4]
{Hankley90} W. Hankley and J. Peters, Temporal Specification of Ada Tasks, HICSS-23, 1990
[5]
{Hatley84} D. Hatley, The Use of Structured Methods in the Development of Large Software Based Avionics Systems, AIAA/IEEE sixth Digital Avionics Systems Conf., 1984
[6]
{Honiden90} S. Honiden et al., An Application of Structural Modeling and Automated Reasoning to Real-Time Systems Design, The Journal of Real-Time Systems, Vol. 1, No. 3, 1990
[7]
{Iso89} ISO, Information Processing Systems-Open Systems Interconnection-LOTOS-A Formal Description Technique Based on the Temporal Ordering of Observational Behavior, ISO8807, 1989
[8]
{Kramer87} B. Kramer, SEGRAS-A Formal and Semigraphical Language combining Petri Nets and Abstract Data Types for the Specification of Distributed Systems, 9th ICSE, 1987
[9]
{Meiling87} E. Meiling, A spreadsheet specification in RSL-an illustration of the RAISE specification language, In ESPRIT'87 Achievements and Impact, North-Holland, pp. 466--479, 1987.
[10]
{Pletat86} U. Pletat, Algebraic specification of abstract data types and CCS: An operational junction, In Protocol Specification, Testing and Verification, Elsevier science Publishers, 1986
[11]
{Problem87} Problem set, Proc. of Fourth International Workshop on Software Specification and Design, CS Press, Los Alamitos, Calif. 1987
[12]
{Vautherin87} J. Vautherin, Parallel Systems Specifications with Coloured Petri Nets and Algebraic Specification, LNCS 266, 1987
[13]
{Ward86} P. Ward, The Transformation Schema: An Extension of the Data Flow Diagram to Represent Control and Timing, IEEE Trans. Software Eng., Vol. 12, No. 2, 1986
[14]
{Ward89} P. Ward, How to Integrate Object Orientation with Structured Analysis and Design, IEEE Software, Vol. 6, No. 2, 1989
[15]
{Wolper83} P. Wolper et al., Synthesis of Communicating Processes from Temporal Logic Specification, ACM TOPLAS, Vol. 6, No. 1, 1983
- An integration environment to put formal specifications into practical use in real-time systems
Recommendations
Real-time specifications
A specification theory combines notions of specifications and implementations with a satisfaction relation, a refinement relation, and a set of operators supporting stepwise design. We develop a specification framework for real-time systems using Timed ...
An Operational Semantics and Compiler for Real-Time Specifications
The Modechart specification language is a formalism for the specification and implementation of real-time systems. This paper presents the semantics for Modechart in an operational style and a compiler for automatically synthesizing specifications. ...
Comments
Information & Contributors
Information
Published In
October 1991
257 pages
ISBN:0818623209
- General Chair:
- Jean-Pierre Finance,
- Program Chairs:
- Carlo Ghezzi,
- Gruia-Catalin Roman
Sponsors
- SIGSOFT: ACM Special Interest Group on Software Engineering
- IEEE-CS\DATC: IEEE Computer Society
Publisher
IEEE Computer Society Press
Washington, DC, United States
Publication History
Published: 25 October 1991
Check for updates
Qualifiers
- Article
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 103Total Downloads
- Downloads (Last 12 months)2
- Downloads (Last 6 weeks)0
Reflects downloads up to 22 Dec 2024
Other Metrics
Citations
View Options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in