------------------------------------------------------------------------------ ------------------------------------------------------------------------------ -- Cheddar is a GNU GPL real-time scheduling analysis tool. -- This program provides services to automatically check schedulability and -- other performance criteria of real-time architecture models. -- -- Copyright (C) 2002-2020, Frank Singhoff, Alain Plantec, Jerome Legrand, -- Hai Nam Tran, Stephane Rubini -- -- The Cheddar project was started in 2002 by -- Frank Singhoff, Lab-STICC UMR CNRS 6285, Universite de Bretagne Occidentale -- -- Cheddar has been published in the "Agence de Protection des Programmes/France" in 2008. -- Since 2008, Ellidiss technologies also contributes to the development of -- Cheddar and provides industrial support. -- -- The full list of contributors and sponsors can be found in AUTHORS.txt and SPONSORS.txt -- -- This program is free software; you can redistribute it and/or modify -- it under the terms of the GNU General Public License as published by -- the Free Software Foundation; either version 2 of the License, or -- (at your option) any later version. -- -- This program is distributed in the hope that it will be useful, -- but WITHOUT ANY WARRANTY; without even the implied warranty of -- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the -- GNU General Public License for more details. -- -- You should have received a copy of the GNU General Public License -- along with this program; if not, write to the Free Software -- Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA -- -- -- Contact : cheddar@listes.univ-brest.fr -- ------------------------------------------------------------------------------ -- Last update : -- $Rev$ -- $Date$ -- $Author: singhoff $ ------------------------------------------------------------------------------ ------------------------------------------------------------------------------ with systems; use systems; with Ada.Strings.Unbounded; use Ada.Strings.Unbounded; with unbounded_strings; use unbounded_strings; with task_set; use task_set; with object_set; use object_set; with time_unit_events; use time_unit_events; with scheduler; use scheduler; with Ada.Real_Time; use Ada.Real_Time; with Ada.Calendar; with Ada.Calendar.Formatting; with Ada.Text_IO; use Ada.Text_IO; package scheduling_anomalies_services is ---------------------------------------- -- Type defining the kind of anomaly ---------------------------------------- type potential_anomaly_type is (no_potential_anomaly, processor_speed_increase, processor_add, task_execution_time_decrease, task_period_increase, task_late_execution, task_priority_change, precedence_constraint_change); ----------------------------------------- -- Runtime verification ----------------------------------------- -- This data stucture is returned after runtime analysis -- with the detected anomaly and the associated data -- type handler_output_parameter is record -- The type of the potential anomalie we found -- detected_anomaly : potential_anomaly_type; -- Give the name of the Cheddar object that create the anomaly -- object_name : unbounded_string; end record; -- This data structure contains the data provided by the -- Cheddar scheduling simulator or the RTOS to perform -- the runtime verification -- type handler_input_parameter is record -- Event produced by the RTOS or the Cheddar simulator -- that requires runtime verification -- event : time_unit_event_ptr; -- Simulation or RTOS data -- runtime_data : scheduling_information; -- Time at which the event is generated -- current_time : Natural; end record; -- Subprogram called before scheduling simulation -- to provide the architecture model before simulation -- procedure initialize(model : in system); -- This subprogram is called by the OS or Cheddar to verify -- at any time if an anomaly will occur -- procedure dynamically_check_anomaly (inp : in handler_input_parameter; current_scheduler : in generic_scheduler'class; outp : out handler_output_parameter); -- Subprograms constituting the implementation -- of the handler -- procedure check_dynamic_processor_speed_increase (inp : in handler_input_parameter; current_scheduler : in generic_scheduler'class; outp : out handler_output_parameter); procedure check_dynamic_processor_add (inp : in handler_input_parameter; outp : out handler_output_parameter); procedure check_dynamic_task_execution_time_decrease (inp : in handler_input_parameter; outp : out handler_output_parameter); procedure check_dynamic_task_period_increase (inp : in handler_input_parameter; outp : out handler_output_parameter); procedure check_dynamic_task_late_execution (inp : in handler_input_parameter; outp : out handler_output_parameter); procedure check_dynamic_task_priority_change (inp : in handler_input_parameter; outp : out handler_output_parameter); procedure check_dynamic_precedence_constraint_change (inp : in handler_input_parameter; outp : out handler_output_parameter); ---------------------------------------- -- Design time verification ---------------------------------------- function print_duration_time_exec return String; ----- Entry point of the static verification -- procedure scheduling_anomalies_analyzer (a_system : in system; msg : out Unbounded_String); procedure check_static_constraint (a_system : in system; to_check : in potential_anomaly_type; result : out Boolean); ----- Subprograms to statically verify each constraint -- function check_c1_mono_processor_system (a_system : in system) return Boolean; function check_c2_multiprocessor_system (a_system : in system) return Boolean; function check_c3_partitionned_scheduling (a_system : in system) return Boolean; function check_c4_global_scheduling (a_system : in system) return Boolean; function check_c5_fixed_priority (a_system : in system) return Boolean; function check_c6_edf_algorithm (a_system : in system) return Boolean; function check_c7_dm_algorithm (a_system : in system) return Boolean; function check_c8_preemptive_processor (a_system : in system) return Boolean; function check_c9_non_preemptive_processor (a_system : in system) return Boolean; function check_c10_synchronous_departure (a_system : in system) return Boolean; function check_c11_asynchronous_departure (a_system : in system) return Boolean; function check_c12_tasks_are_periodic (a_system : in system) return Boolean; function check_c13_tasks_are_independent (a_system : in system) return Boolean; function check_c14_tasks_are_suspended (a_system : in system) return Boolean; function check_c15_tasks_have_precedence_constraint (a_system : in system) return Boolean; function check_c16_tasks_have_shared_resouces (a_system : in system) return Boolean; function check_c17_tasks_are_aperiodic (a_system : in system) return Boolean; ----- Subprograms to statically verify each anomaly -- function check_static_processor_speed_increase (a_system : in system) return Boolean; function check_static_task_execution_time_decrease (a_system : in system) return Boolean; function check_static_processor_add (a_system : in system) return Boolean; function check_static_task_period_increase (a_system : in system) return Boolean; function check_static_task_late_execution (a_system : in system) return Boolean; function check_static_task_priority_change (a_system : in system) return Boolean; function check_static_precedence_constraint_change (a_system : in system) return Boolean; end scheduling_anomalies_services;