CFP last date
20 May 2024
Reseach Article

Article:How to Make AADL Specification More Precise

by M. Benammar, F. Belala
International Journal of Computer Applications
Foundation of Computer Science (FCS), NY, USA
Volume 8 - Number 10
Year of Publication: 2010
Authors: M. Benammar, F. Belala
10.5120/1243-1756

M. Benammar, F. Belala . Article:How to Make AADL Specification More Precise. International Journal of Computer Applications. 8, 10 ( October 2010), 16-23. DOI=10.5120/1243-1756

@article{ 10.5120/1243-1756,
author = { M. Benammar, F. Belala },
title = { Article:How to Make AADL Specification More Precise },
journal = { International Journal of Computer Applications },
issue_date = { October 2010 },
volume = { 8 },
number = { 10 },
month = { October },
year = { 2010 },
issn = { 0975-8887 },
pages = { 16-23 },
numpages = {9},
url = { https://ijcaonline.org/archives/volume8/number10/1243-1756/ },
doi = { 10.5120/1243-1756 },
publisher = {Foundation of Computer Science (FCS), NY, USA},
address = {New York, USA}
}
%0 Journal Article
%1 2024-02-06T19:57:25.442532+05:30
%A M. Benammar
%A F. Belala
%T Article:How to Make AADL Specification More Precise
%J International Journal of Computer Applications
%@ 0975-8887
%V 8
%N 10
%P 16-23
%D 2010
%I Foundation of Computer Science (FCS), NY, USA
Abstract

AADL (Architectural Analysis and Design Language) is a textual and graphical language used to design and analyze software architecture of embedded real time systems. Many tools and models provide semantics and precise meaning for AADL architecture behavior. However, they are not supported by a well defined formal semantics. This paper suggets Rewriting Logic via its practical language Maude as an adequate formalism for modeling behavior concepts in an AADL architectural description. Besides, RT-Maude system offers a natural support to execute and prototype real-time object-oriented modules formalizing AADL architecture behavior composed of several communicating threads.

References
  1. SAE International 2008 Architecture Analysis and Design Language (AADL) Standard, Version 2. SAE Draft Standard AS5506 V2.
  2. Dissaux, P., Bodeveix, J.P., Filali, M., Gaufillet, P., and Vernadat, F. 2006 AADL Behavioral Annex. In Proceeding of the DASIA’06, Data Systems in Aerospace- Conference, Berlin, Germany, ESA SP-630.
  3. Ölveczky, P. C. 2007 Real-Time Maude 2.3 Manual. Department of Informatics, University of Oslo.
  4. Clavel, M., Duran, F., Eker, S., Marti-Oliet, N., Lincoln, P., Meseguer, J., and Talcott, C. 2008 Maude Manual (Version 2.4).
  5. Meseguer, J. 1992 Conditional rewriting logic as a unified model of concurrency. Theoretical Computer Science, 96(1), pp. 73-155.
  6. Marti-Oliet, N., Meseguer, J. 1993 Rewriting logic as logical and semantic framework. Technical Report SRI-CSL-93-05, SRI International, Computer Science Laboratory.
  7. Bruni, R., Meseguer, J. 2006 Semantic foundations for generalized rewrite theories. Theoretical Computer Science 360, pp. 386-414.
  8. Clavel, M., Duran, F., Eker, S., Lincoln, P., Marti-Oliet, N., Meseguer, J., Quesada, J. F. 2002 Maude: Specification and programming in rewriting logic”, Theoretical Computer Science, pp. 187–243.
  9. Ölveczky, P. C., Meseguer, J., and Talcott, C. 2006 Specification and Analysis of the AER/NCA Active Network Protocol suite in Real-Time Maude. In Formal Methods in System Design, vol. 29, pp. 253-293.
  10. Ölveczky, P. C., and Caccamo, M. 2006 Formal Simulation and Analysis of CASH Scheduling algorithm in Real-Time Maude. Electronic Notes in Theoretical Computer Science, L. Baresi and R. Heckel editors, Vol. 3922, pp. 357-372.
  11. Ölveczky, P. C., and Thorvaldsen, S. 2006 Formal Modeling and Analysis of Wireless Sensor Network Algorithms in Real-Time Maude. In IPDPS’2006: Parallel and Distributed processing Symposium.
  12. Jerad, C., Barkaoui, K., and Grissa-Touzi, A.. 2007 Hierarchical Verification in Maude of LfP Software Architectures. In ECSA'07, 1st European Conference on Software Architecture, Aranjuez (Madrid), LNCS , Springer, pp. 156-170
  13. Barkaoui, K., Boucheneb, H., and Hicheur, A. 2008 Modeling and Analyzing Time-Contrained Flexible Workflows with Time Recursive Petri Nets. In 5th International Workshop on Web Services and Formal Methods Co-Located with BPM 2008, LNCS volume 5387, Springer R. Bruni, pp. 19-35.
  14. Berthomieu, B., Ribet, P.-O., and Vernadat, F. 2004 The tool TINA-construction of abstract state spaces for Petri nets and time Petri nets, International Journal of Production Research, Vol. 42, pp. 2741-2756.
  15. Garavel, H., Mateescu, R., Lang, F., Serwe, W. 2007 CADP 2006 : A toolbox for the construction and analysis of distributed processes, In Werner Damm and Holger Hermanns editors CAV, LNCS, Springer vol. 4590, pp. 158-163.
  16. Chkouri, M., Robert, A., Bozga, M., and Sifakis, J. 2008 Translating AADL into BIP -Application to the Verification of Real-time Systems, In Proc. of MoDELSACES-MB Model Based Architecting and Construction of Embedded Systems, pp. 39-54.
  17. Renault, X., Kordon,, F., Hugues, J. 2009 Adapting models to modelcheckers, a case study : Analyzing AADL using Time or Colored Petri Nets. In Proceedings of the 20th International Symposium on Rapid System Prototyping, IEEE Computer Society, pp. 26-33.
  18. Renault, X., Kordon, F., Hugues, J. 2009 From AADL architectural models to Petri Nets: Checking model viability. 12th IEEE International Symposium on Object-oriented Real-time distributed Computing (ISORC'09), IEEE Computer Society, pp. 313-320.
  19. Sokolsky, O., Lee, I., and Clarke, D. 2009 Process-Algebraic Interpretation of AADL Models. 14th International Conference on Reliable Software Technologies, LNCS 5570, pp. 222-236
  20. Yang, Z., Hu, K., Ma, D., and Pi, L. 2009 Towards a Formal Semantics for The AADL Behavior Annex. In Design, Automation & Test in Europe DATE 2009, pp. 1166-1171.
Index Terms

Computer Science
Information Sciences

Keywords

AADL Behavioral Annex Revised Rewriting Logic Real Time Maude