A formal design notation for real-time systems

The development of real-time systems is based on a variety of different methods and notations. Despite the purported benefits of formal methods, informal techniques still play a predominant role in current industrial practice. Formal and informal methods have been combined in various ways to smoothl...

Descripción completa

Guardado en:
Detalles Bibliográficos
Autor principal: Felder, M.
Otros Autores: Pezzè, M.
Formato: Capítulo de libro
Lenguaje:Inglés
Publicado: Association for Computing Machinery 2002
Acceso en línea:Registro en Scopus
DOI
Handle
Registro en la Biblioteca Digital
Aporte de:Registro referencial: Solicitar el recurso aquí
LEADER 09961caa a22009977a 4500
001 PAPER-5394
003 AR-BaUEN
005 20230518203502.0
008 190411s2002 xx ||||fo|||| 00| 0 eng|d
024 7 |2 scopus  |a 2-s2.0-11244315081 
040 |a Scopus  |b spa  |c AR-BaUEN  |d AR-BaUEN 
030 |a ATSME 
100 1 |a Felder, M. 
245 1 2 |a A formal design notation for real-time systems 
260 |b Association for Computing Machinery  |c 2002 
270 1 0 |m Felder, M.; Departamento de Computacion-FCEN, Universidad de Beunos Aires, Ciudad Universitaria, 1428 Buenos Aires, Argentina; email: felder@dc.uba.ar 
506 |2 openaire  |e Política editorial 
504 |a Alur, R., Courcoubetis, C., Dill, D., Model Checking for Real-Time Systems (1990) Proceedings of the IEEE 5th Annual Symposium on Logic in Computer Science 
504 |a Baresi, L., Orso, A., Pezzè, M., Introducing Formal Methods in Industrial Practice (1997) Proceedings of the 20th International Conference on Software Engineering (ICSE'97), pp. 56-66. , ACM Press (May) 
504 |a Baresi, L., Pezzè, M., On Formalizing UML with High Level Petri Nets (2001) Lecture Notes in Computer Sciences, 2001. , Concurrent Object-Oriented Programming and Petri Nets, G. A. Agha, F. De Cindio, G. Rozenberg, Eds. Springer-Verlag 
504 |a Burgueo, A., Rusu, V., Task-system analysis using Slope-Parametric Hybrid Automata (1997) Proceedings of the Euro-Par'97 Workshop on Real-Time Systems and Constraints, , Passau, Germany (August 26-29) 
504 |a Burns, A., Wellings, A.J., (1993) HRT-HOOD: A Structure Design Method for Hard Real-Time Systems, , YCS-93-199, York University 
504 |a Cheng, S., Stankovic, J.A., Scheduling Algorithm for Hard Real-Time Systems - A Brief Summary (1988) Hard Real-Time Systems Tutorial, , Stankovic and Ramaritham editors, IEEE Computer Society 
504 |a Corbett, J., Timing Analysis of Ada Tasking Programs (1996) IEEE Transactions on Software Engineering, 22 (7 JULY) 
504 |a Douglass, B.P., (1998) Real-time UML: Developing Efficient Objects for Embedded Systems, , Addison Wesley 
504 |a Duri, S., Buy, U., Devarapalli, R., Shatz, S., Using State Space Reduction Methods for Deadlock Analysis in Ada Tasking (1993) Proceedings of the International Symposium on Software Testing and Analysis, , ISSTA'93, June 
504 |a Elsistrøm, R., Lintulampi, R., Pezzè, M., Giving Semantics to SA/RT by Means of High-Level Timed Petri Nets (1993) J. Real-Time Syst., 5 (2-3), pp. 249-272. , May 
504 |a Felder, M., Ghezzi, C., Pezzè, M., Analyzing Requirements of State-Based Specifications: The Case of TB Nets (1993) Proceedings International Symposium on Software Testing and Analysis (ISSTA), , Cambridge, MA (June) 
504 |a Felder, M., Pezzè, M., RTD: A design notation for Structured Analysis Real-Time (1997) Proceedings of the KIT125 Workshop on Formal Methods for the Design of Real-Time Systems, , Como (Sept.) 
504 |a France, R.B., Semantically Extended Data Flow Diagrams: A Formal Specification Tool (1992) IEEE Trans. Softw. Eng., 18 (4 APR.) 
504 |a France, R.B., Larrondo-Petrie, M.M., From Structured Analysis to Formal Specifications: State of the Theory (1994) Proceedings of the ACM Computer Science Conference, pp. 249-256. , April, ACM Press 
504 |a Fraser, M.D., Kumar, K., Vaishnavi, V.K., Informal and Formal Requirements Specification Languages: Bridging the Gap (1991) IEEE Trans. Softw. Eng., 17 (5 MAY), pp. 454-466 
504 |a Fredette, A.N., Cleaveland, R., RTSL: A Formal Language for Real-Time Schedulability Analysis (1993) Proceedings of the Real-Time Systems Symposium, pp. 274-283. , Durham, NC (Dec.), Computer Society Press 
504 |a Ghezzi, C., Jazayeri, M., Mandrioli, D., (1991) Fundamentals of Software Engineering, , Prentice Hall, Englewood Cliffs, NJ 
504 |a Ghezzi, C., Mandrioli, D., Morasca, S., Pezzè, M., A Unified High-Level Petri-Net Formalism for Time-Critical Systems (1991) IEEE Trans. Softw. Eng., 17. , Feb 
504 |a Ghezzi, C., Mandrioli, D., Morzenti, A., TRIO, a Logic Language for Executable Specifications of Real-Time Systems (1990) J. Sys. Softw., , May 
504 |a Ghezzi, C., Morasca, S., Pezzè, M., Timing Analysis of Time Basic Nets (1994) J. Sys. Softw., 27 (7 NOV.) 
504 |a Gomaa, H., (1993) Software Design Methods for Concurrent and Real-Time Systems, , Addison Wesley 
504 |a Harel, D., Statecharts: A Visual Formalism for Complex Systems (1987) Science of Computer Programming, 8 
504 |a Hatley, D.J., Pirbhai, I.A., (1987) Strategies for Real-Time System Specification, , Dorset House, New York 
504 |a Houstin, C., Module Allocation of Real-Time Applications to Distributed Systems (1990) IEEE Trans. Softw. Eng., 16 (7 JULY) 
504 |a Real-Time Extensions to POSIX (1993) IEEE Standard P1003.1b, , IEEE Press (March) 
504 |a Jackson, M., (1983) System Development, , Prentice Hall, Englewood Cliffs, NJ 
504 |a Jensen, K., Coloured Petri Nets (1996) Monographs in Theoretical Computer Science, Second Edition, , Springer-Verlag, Berlin 
504 |a Jones, C.B., (1989) Systematic Software Development Using VDM, , Prentice-Hall, Englewood Cliffs, NJ 
504 |a Kronlöf, C., (1993) Method Integration - Concepts and Case Studies, , John Wiley & Sons 
504 |a Liu, L.Y., Shyamasundar, R.K., Static Analysis of Real-Time Distributed Systems (1990) IEEE Trans. Softw. Eng., 16, p. 4 
504 |a Moser, L.E., Ramakrishna, Y.S., Kutty, G., Melliar-Smith, P.M., Dillon, L.K., A Graphical Environment for the Design of Concurrent Real-Time Systems (1997) ACM Trans. Softw. Eng. Methodol., 6 (1 JAN.) 
504 |a Nissanke, N., (1997) Realtime Systems, , Prentice Hall, Englewood Cliffs, NJ 
504 |a Palis, M.A., Liou, J.-C., Wei, D.S.L., Task Clustering and Scheduling for Distributed Memory Parallel Architectures (1996) IEEE Trans. Para. Distrib. Syst., 7 (1 JAN) 
504 |a Pezzè, M., Ghezzi, C., Cabernet: An Environment for the Specification and Verification of Real-Time Systems (1992) Proceeding of DECUS Europe Symposium, , Cannes (France, Sept.) 
504 |a Richter, G., Maffeo, B., Toward a Rigorous Interpretation of ESML - Extended Systems Modeling Language (1993) IEEE Trans. Softw. Eng., 19 (2 FEB.) 
504 |a Stankovic, J.A., Spuri, M., Di Natale, M., Buttazzo, C., Implication of Classical Scheduling Results for Real-Time Systems (1995) IEEE Computer, pp. 16-25. , June 
504 |a Valmari, A., A Stubborn Attach to State Explosion (1991) Proceedings of the 2nd International Workshop on Computer-Aided Verification, , LNCS 531, Springer-Verlag 
504 |a Wang, E.Y., Richter, H.A., Cheng, B.H.C., Formalizing and Integrating the Dynamic Model with OMT (1997) Proceedings of the 20th International Conference on Software Engineering (ICSE), pp. 45-55. , ACM Press 
504 |a Ward, P.T., Mellor, S.J., (1985) Structured Development for Real-Time Systems, , Yourdon Press Computing Series 
504 |a Wing, J.M., Zaremski, A.M., Two Ways to Integrate Formal Specifications in Practice (1991) Proceedings of Formal Methods Europe 
504 |a Yeh, W.J., Young, M., Compositional Reachability Analysis Using Process Algebra (1991) Proceedings of the International Testing and Analysis Workshop (TAV 4), , ACM Press (Oct.) 
520 3 |a The development of real-time systems is based on a variety of different methods and notations. Despite the purported benefits of formal methods, informal techniques still play a predominant role in current industrial practice. Formal and informal methods have been combined in various ways to smoothly introduce formal methods in industrial practice. The combination of real-time structured analysis (SA-RT) with Petri nets is among the most popular approaches, but has been applied only to requirements specifications. This paper extends SA-RT to specifications of the detailed design of embedded real-time systems, and combines the proposed notation with Petri nets.  |l eng 
593 |a Universitad de Buenos Aires, Argentina 
593 |a Univ. Studi di Milano - Bicocca, Italy 
593 |a Departamento de Computacion-FCEN, Universidad de Beunos Aires, Ciudad Universitaria, 1428 Buenos Aires, Argentina 
593 |a Dipartimento di Informatica, Univ. degli Studi di Milano-Bicocca, Via Bicocca degli Arcimboldi, 8, I-2026 Milano, Italy 
690 1 0 |a DESIGN OF REAL TIME SYSTEMS 
690 1 0 |a FORMAL ANALYSIS OF DESIGN SPECIFICATION 
690 1 0 |a FORMAL DESIGN SPECIFICATION 
690 1 0 |a STRUCTURED DESIGN 
690 1 0 |a DESIGN OF REAL TIME SYSTEMS 
690 1 0 |a FORMAL ANALYSIS OF DESIGN SPECIFICATION 
690 1 0 |a FORMAL DESIGN SPECIFICATION 
690 1 0 |a STRUCTURED DESIGN 
690 1 0 |a EMBEDDED SYSTEMS 
690 1 0 |a PETRI NETS 
690 1 0 |a REAL TIME SYSTEMS 
690 1 0 |a STRUCTURAL DESIGN 
690 1 0 |a STRUCTURED PROGRAMMING 
690 1 0 |a SOFTWARE ENGINEERING 
700 1 |a Pezzè, M. 
773 0 |d Association for Computing Machinery, 2002  |g v. 11  |h pp. 149-190  |k n. 2  |p ACM Trans Software Eng Methodol  |x 1049331X  |w (AR-BaUEN)CENRE-1081  |t ACM Transactions on Software Engineering and Methodology 
856 4 1 |u https://www.scopus.com/inward/record.uri?eid=2-s2.0-11244315081&doi=10.1145%2f505145.505146&partnerID=40&md5=ce423088beaf771fcc462cc5bda9f6e2  |y Registro en Scopus 
856 4 0 |u https://doi.org/10.1145/505145.505146  |y DOI 
856 4 0 |u https://hdl.handle.net/20.500.12110/paper_1049331X_v11_n2_p149_Felder  |y Handle 
856 4 0 |u https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_1049331X_v11_n2_p149_Felder  |y Registro en la Biblioteca Digital 
961 |a paper_1049331X_v11_n2_p149_Felder  |b paper  |c PE 
962 |a info:eu-repo/semantics/article  |a info:ar-repo/semantics/artículo  |b info:eu-repo/semantics/publishedVersion 
999 |c 66347