A language and a pattern system for temporal property specification: advanced metering infrastructure case study
- PDF / 802,895 Bytes
- 16 Pages / 595.276 x 790.866 pts Page_size
- 40 Downloads / 203 Views
REGULAR CONTRIBUTION
A language and a pattern system for temporal property specification: advanced metering infrastructure case study Tina Tavizi1 · Mehdi Shajari1
© Springer-Verlag GmbH Germany, part of Springer Nature 2020
Abstract Ensuring the satisfaction of security requirements is one of the most vital needs in developing different types of systems. Therefore, it is necessary to apply a method to accurately define security requirements and then, verify them in the design phase before starting system development. One of the key information security requirements is availability of system functionalities for authorized users. This type of requirement is especially important in real-time embedded systems (RTESs) because they are associated with hard temporal needs and deadlines, and if they are not satisfied the main functionality of the system will be interrupted. To make sure that the availability properties are correctly considered in the design of a system, a language is needed to specify different temporal constraints. This language should be applicable for system designers who do not have sufficient formal and mathematical knowledge. OCL is a high-level constraint specification language (based on UML modeling language) which is widely used by system designer teams, and therefore, it is appropriate for this purpose. However, OCL does not support specification of temporal properties. In this paper, using a hybrid logic-based and pattern-based approach, a language grammar based on OCL, named RTSL has been proposed. RTSL is able to specify different real-time temporal properties. To achieve this goal, we developed a comprehensive property specification pattern system which considers all qualitative, quantitative and probabilistic property patterns that is used as a guideline for property specification and language development. Keywords Real-time embedded system · Property specification language · Pattern system · OCL
1 Introduction Verification of security properties in early stages of system development is one of the most critical requirements that results in more secure systems. System developers usually postpone security testing to final stages of development lifecycle resulting in a unreliable and costly patching process. Secure system design is an emerging paradigm in secure software/hardware development that provides tools and procedures for system production teams to verify their design specifications against the required security properties. In this approach, system specification is modeled with a formal specification language, and then, a formal verification tool
B
Mehdi Shajari [email protected] Tina Tavizi [email protected]
1
Amirkabir University of Technology, Tehran, Iran
checks if the model meets a given specification before the team starts implementing a vulnerable model of the system. Availability properties are among the least addressed properties in different aspects of formal security verification approaches. The lack of a proper system/property specification language is on
Data Loading...
