------------------------------------------------------------------------------ ------------------------------------------------------------------------------ -- 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 anomaly_type is ( 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 anomalie we found -- detected_anomaly : anomaly_type; -- Give the list of Cheddar objects that create the anomaly -- origine_object : objects_set; -- Give the list of task that will missed their deadline -- because of the anomaly -- missed_deadline : tasks_set; 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; end record; -- 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; outp : out handler_output_parameter); -- Subprograms constituting the implementation -- of the handler -- procedure handler_processor_speed_increase (inp : in handler_input_parameter; outp : out handler_output_parameter); procedure handler_processor_add (inp : in handler_input_parameter; outp : out handler_output_parameter); procedure handler_task_execution_time_decrease (inp : in handler_input_parameter; outp : out handler_output_parameter); procedure handler_task_period_increase (inp : in handler_input_parameter; outp : out handler_output_parameter); procedure handler_task_late_execution (inp : in handler_input_parameter; outp : out handler_output_parameter); procedure handler_task_priority_change (inp : in handler_input_parameter; outp : out handler_output_parameter); procedure handler_precedence_constraint_change (inp : in handler_input_parameter; outp : out handler_output_parameter); procedure handler_task_activation(inp : in handler_input_parameter; outp : out handler_output_parameter); procedure handler_running_task(inp : in handler_input_parameter; outp : out handler_output_parameter); procedure handler_start_of_task_capacity(inp : in handler_input_parameter; outp : out handler_output_parameter); procedure handler_end_of_task_capacity(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 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;