TY - JOUR
T1 - A formal approach for the specification and verification of trustworthy component-based systems
AU - Mohammad, Mubarak
AU - Alagar, Vangalur
PY - 2011/1
Y1 - 2011/1
N2 - Software systems are increasingly becoming ubiquitous affecting the way we experience the world. Embedded software systems, especially those used in smart devices, have become an essential constituent of the technological infrastructure of modern societies. Such systems, in order to be trusted in society, must be proved to be trustworthy. Trustworthiness is a composite non-functional property that implies safety, timeliness, security, availability, and reliability. This paper presents a formal approach for the development of trustworthy component-based systems. The approach involves a formal component model for the specification of component's structure, functional, and non-functional (trustworthiness) properties, a model transformation technique for the automatic generation of component behavior using the specified structure and restricted by the specified properties, and a unified formal verification method for safety, security, reliability and availability properties using model checking.
AB - Software systems are increasingly becoming ubiquitous affecting the way we experience the world. Embedded software systems, especially those used in smart devices, have become an essential constituent of the technological infrastructure of modern societies. Such systems, in order to be trusted in society, must be proved to be trustworthy. Trustworthiness is a composite non-functional property that implies safety, timeliness, security, availability, and reliability. This paper presents a formal approach for the development of trustworthy component-based systems. The approach involves a formal component model for the specification of component's structure, functional, and non-functional (trustworthiness) properties, a model transformation technique for the automatic generation of component behavior using the specified structure and restricted by the specified properties, and a unified formal verification method for safety, security, reliability and availability properties using model checking.
KW - Component model
KW - Component-based development
KW - Formal verification
KW - Trustworthiness
UR - http://www.scopus.com/inward/record.url?scp=78649326944&partnerID=8YFLogxK
U2 - 10.1016/j.jss.2010.08.048
DO - 10.1016/j.jss.2010.08.048
M3 - Article
AN - SCOPUS:78649326944
SN - 0164-1212
VL - 84
SP - 77
EP - 104
JO - The Journal of Systems and Software
JF - The Journal of Systems and Software
IS - 1
ER -